Convex hulls of points and directions

Convex analysis works throughout with the convex hull of a set S that mixes points and directions (points at infinity): conv S is the smallest convex set that contains every point of S and recedes in every direction of S, and it equals conv S₀ + cone S₁. This file supplies that object and its API.

A set of directions is represented by a set of vectors, one or more per direction: cone D, and hence convexHullPD P D, depends only on the directions of the vectors in D, so nothing is lost and no quotient type is needed. Note that convexHullPD ∅ D = ∅ — a set of directions alone has empty convex hull, since the empty set recedes in every direction — which is Rockafellar's convention.

Main definitions

• convexHullPD P D — the convex hull of the points P together with the directions of the vectors in D, defined as conv P + cone D.
• halfLine x y — the closed half-line from x in the direction of y. It is conv S for a one-point, one-direction S, and it is the shape of the faces that carry the extreme and exposed directions of a convex set.
• coneOverPD P D — the cone over conv S in ℝ × E, enlarged by its level-zero directions; the auxiliary object in the proof of the homogenisation dictionary.
• affineSpanPD P D, finrankPD P D — the affine hull aff S = aff (conv S) and its dimension.
• AffineIndepPD P D — affine independence of a mixed set: the homogenisation is linearly independent in ℝ × E.
• IsSimplexPD m C — a generalized m-dimensional simplex, the convex hull of m + 1 affinely independent points and directions.

Main results

• isLeast_convexHullPD — convexHullPD P D is Rockafellar's definition: the least convex set containing P and receding in every direction of D. Everything else follows from that IsLeast pair.
• convexHullPD_eq_slice — the homogenisation dictionary: conv S is the level-one slice of the pointed cone in ℝ × E generated by liftPD P D = ({1} × P) ∪ ({0} × D).
• exists_of_mem_convexHullPD — Carathéodory's theorem for points and directions.
• IsCompact.isClosed_convexHullPD — conv P + cone D is closed when P is compact and cone D is closed.
• finrank_span_liftPD — the homogenisation raises the dimension by exactly one, dim K = d + 1; this is what makes the padding step of Carathéodory's theorem possible.
• convexHullPD_eq_iUnion_simplex — conv S is the union of the generalized d-dimensional simplices with vertices in S, d = dim (conv S).
• finrankPD_add_one_of_affineIndepPD, finrank_vectorSpan_of_isSimplexPD — a generalized m-dimensional simplex has dimension m, recovering Rockafellar's own definition of affine independence for a mixed set.

Implementation notes

Rockafellar defines conv S by its minimality property and derives conv S₀ + cone S₁. Here the formula is the definition, because it is what every proof manipulates, and isLeast_convexHullPD recovers the minimality property. Polyhedral/Defs.lean's FinitelyGenerated C is definitionally ∃ P D : Finset E, C = convexHullPD ↑P ↑D, but sits above this file in the import order and so carries its own copy of the homogenisation dictionary.

References

• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §17.

The definition

def Tdaf.ConvexAnalysis.convexHullPD {E : Type u_1} [AddCommGroup E] [Module ℝ E] (P D : Set E) : Set E

The convex hull of a set of points and directions. convexHullPD P D is the smallest convex set containing the points P and receding in the direction of every vector of D; it is conv P + cone D, Rockafellar's own formula (isLeast_convexHullPD proves the two agree). Directions are represented by vectors, since cone D is unchanged by rescaling a generator.

Equations

• Tdaf.ConvexAnalysis.convexHullPD P D = (convexHull ℝ) P + ↑(PointedCone.hull ℝ D)

theorem Tdaf.ConvexAnalysis.convexHullPD_def {E : Type u_1} [AddCommGroup E] [Module ℝ E] (P D : Set E) : convexHullPD P D = (convexHull ℝ) P + ↑(PointedCone.hull ℝ D)

conv S unfolded: the Minkowski sum of the convex hull of the points and the cone hull of the directions.

theorem Tdaf.ConvexAnalysis.mem_convexHullPD {E : Type u_1} [AddCommGroup E] [Module ℝ E] {P D : Set E} {x : E} : x ∈ convexHullPD P D ↔ ∃ u ∈ (convexHull ℝ) P, ∃ v ∈ ↑(PointedCone.hull ℝ D), u + v = x

Membership in conv S: a point of the convex hull of P plus a direction of cone D.

theorem Tdaf.ConvexAnalysis.convexHull_subset_convexHullPD {E : Type u_1} [AddCommGroup E] [Module ℝ E] (P D : Set E) : (convexHull ℝ) P ⊆ convexHullPD P D

The convex hull of the points alone is contained in the hull of the points and directions.

theorem Tdaf.ConvexAnalysis.subset_convexHullPD {E : Type u_1} [AddCommGroup E] [Module ℝ E] (P D : Set E) : P ⊆ convexHullPD P D

The points of S belong to conv S.

@[simp]

theorem Tdaf.ConvexAnalysis.convexHullPD_empty_right {E : Type u_1} [AddCommGroup E] [Module ℝ E] (P : Set E) : convexHullPD P ∅ = (convexHull ℝ) P

With no directions, conv S is the ordinary convex hull.

@[simp]

theorem Tdaf.ConvexAnalysis.convexHullPD_empty_left {E : Type u_1} [AddCommGroup E] [Module ℝ E] (D : Set E) : convexHullPD ∅ D = ∅

A set of directions alone has empty convex hull, Rockafellar's convention.

theorem Tdaf.ConvexAnalysis.convex_convexHullPD {E : Type u_1} [AddCommGroup E] [Module ℝ E] (P D : Set E) : Convex ℝ (convexHullPD P D)

conv S is convex.

theorem Tdaf.ConvexAnalysis.coneHull_subset_recessionCone_convexHullPD {E : Type u_1} [AddCommGroup E] [Module ℝ E] (P D : Set E) : ↑(PointedCone.hull ℝ D) ⊆ recessionCone (convexHullPD P D)

conv S recedes in every direction of S — indeed in every direction of cone D.

theorem Tdaf.ConvexAnalysis.subset_recessionCone_convexHullPD {E : Type u_1} [AddCommGroup E] [Module ℝ E] (P D : Set E) : D ⊆ recessionCone (convexHullPD P D)

conv S recedes in every direction of S.

theorem Tdaf.ConvexAnalysis.convexHullPD_min {E : Type u_1} [AddCommGroup E] [Module ℝ E] {P D C : Set E} (hC : Convex ℝ C) (hP : P ⊆ C) (hD : D ⊆ recessionCone C) : convexHullPD P D ⊆ C

Minimality: every convex set that contains the points of S and recedes in its directions contains conv S.

theorem Tdaf.ConvexAnalysis.isLeast_convexHullPD {E : Type u_1} [AddCommGroup E] [Module ℝ E] (P D : Set E) : IsLeast {C : Set E | Convex ℝ C ∧ P ⊆ C ∧ D ⊆ recessionCone C} (convexHullPD P D)

Rockafellar's definition of conv S: it is the least convex set containing the points of S and receding in all the directions of S.

theorem Tdaf.ConvexAnalysis.convexHullPD_mono {E : Type u_1} [AddCommGroup E] [Module ℝ E] {P₁ P₂ D₁ D₂ : Set E} (hP : P₁ ⊆ P₂) (hD : D₁ ⊆ D₂) : convexHullPD P₁ D₁ ⊆ convexHullPD P₂ D₂

conv S is monotone in the points and in the directions.

theorem Tdaf.ConvexAnalysis.convexHullPD_mono_left {E : Type u_1} [AddCommGroup E] [Module ℝ E] {P₁ P₂ : Set E} (hP : P₁ ⊆ P₂) (D : Set E) : convexHullPD P₁ D ⊆ convexHullPD P₂ D

Monotonicity in the points.

theorem Tdaf.ConvexAnalysis.convexHullPD_mono_right {E : Type u_1} [AddCommGroup E] [Module ℝ E] {D₁ D₂ : Set E} (P : Set E) (hD : D₁ ⊆ D₂) : convexHullPD P D₁ ⊆ convexHullPD P D₂

Monotonicity in the directions.

@[simp]

theorem Tdaf.ConvexAnalysis.convexHullPD_convexHull {E : Type u_1} [AddCommGroup E] [Module ℝ E] (P D : Set E) : convexHullPD ((convexHull ℝ) P) D = convexHullPD P D

Taking the convex hull of the points first changes nothing.

@[simp]

theorem Tdaf.ConvexAnalysis.convexHullPD_coneHull {E : Type u_1} [AddCommGroup E] [Module ℝ E] (P D : Set E) : convexHullPD P ↑(PointedCone.hull ℝ D) = convexHullPD P D

Taking the cone hull of the directions first changes nothing.

theorem Tdaf.ConvexAnalysis.convexHullPD_add_coneHull {E : Type u_1} [AddCommGroup E] [Module ℝ E] (P D : Set E) : convexHullPD P D + ↑(PointedCone.hull ℝ D) = convexHullPD P D

conv S absorbs its own recession directions: adding cone D again changes nothing.

@[simp]

theorem Tdaf.ConvexAnalysis.convexHullPD_singleton_empty {E : Type u_1} [AddCommGroup E] [Module ℝ E] (x : E) : convexHullPD {x} ∅ = {x}

A singleton of points with no directions.

@[simp]

theorem Tdaf.ConvexAnalysis.convexHullPD_zero_singleton {E : Type u_1} [AddCommGroup E] [Module ℝ E] (D : Set E) : convexHullPD {0} D = ↑(PointedCone.hull ℝ D)

With the origin as its only point, the hull of points and directions is just the cone hull.

theorem Tdaf.ConvexAnalysis.coe_coneHull_singleton {E : Type u_1} [AddCommGroup E] [Module ℝ E] (y : E) : ↑(PointedCone.hull ℝ {y}) = {z : E | ∃ (a : ℝ), 0 ≤ a ∧ z = a • y}

The cone generated by a single vector.

def Tdaf.ConvexAnalysis.halfLine {E : Type u_1} [AddCommGroup E] [Module ℝ E] (x y : E) : Set E

The closed half-line issuing from x in the direction of y. Half-line faces, and with them the extreme and exposed directions of a convex set, are all phrased with it.

Equations

• Tdaf.ConvexAnalysis.halfLine x y = {z : E | ∃ (a : ℝ), 0 ≤ a ∧ z = x + a • y}

theorem Tdaf.ConvexAnalysis.mem_halfLine {E : Type u_1} [AddCommGroup E] [Module ℝ E] {x y z : E} : z ∈ halfLine x y ↔ ∃ (a : ℝ), 0 ≤ a ∧ z = x + a • y

Membership in a half-line, unfolded.

theorem Tdaf.ConvexAnalysis.convexHullPD_singleton {E : Type u_1} [AddCommGroup E] [Module ℝ E] (x y : E) : convexHullPD {x} {y} = halfLine x y

A half-line is the convex hull of one point and one direction.

theorem Tdaf.ConvexAnalysis.left_mem_halfLine {E : Type u_1} [AddCommGroup E] [Module ℝ E] (x y : E) : x ∈ halfLine x y

The endpoint belongs to the half-line.

theorem Tdaf.ConvexAnalysis.convex_halfLine {E : Type u_1} [AddCommGroup E] [Module ℝ E] (x y : E) : Convex ℝ (halfLine x y)

A half-line is convex.

theorem Tdaf.ConvexAnalysis.halfLine_smul {E : Type u_1} [AddCommGroup E] [Module ℝ E] (x y : E) {a : ℝ} (ha : 0 < a) : halfLine x (a • y) = halfLine x y

A half-line depends only on the direction of y.

theorem Tdaf.ConvexAnalysis.mem_recessionCone_halfLine {E : Type u_1} [AddCommGroup E] [Module ℝ E] (x y : E) : y ∈ recessionCone (halfLine x y)

The half-line issuing from x in the direction of y recedes in the direction of y.

theorem Tdaf.ConvexAnalysis.recessionCone_halfLine {E : Type u_1} [AddCommGroup E] [Module ℝ E] (x y : E) : recessionCone (halfLine x y) = {z : E | ∃ (a : ℝ), 0 ≤ a ∧ z = a • y}

The recession cone of a half-line is the ray of its direction.

The homogenisation dictionary

def Tdaf.ConvexAnalysis.coneOverPD {E : Type u_1} [AddCommGroup E] [Module ℝ E] (P D : Set E) : PointedCone ℝ (ℝ × E)

The auxiliary cone behind the homogenisation dictionary: the pairs (a, x) with a > 0 and a⁻¹ • x ∈ conv S, together with the pairs (0, x) with x ∈ cone D. It is the cone over conv S enlarged by its level-zero directions — the largest cone whose level-one slice is still conv S.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Tdaf.ConvexAnalysis.mem_coneOverPD {E : Type u_1} [AddCommGroup E] [Module ℝ E] {P D : Set E} {p : ℝ × E} : p ∈ coneOverPD P D ↔ 0 < p.1 ∧ p.1⁻¹ • p.2 ∈ convexHullPD P D ∨ p.1 = 0 ∧ p.2 ∈ ↑(PointedCone.hull ℝ D)

Membership in coneOverPD, unfolded.

theorem Tdaf.ConvexAnalysis.convexHullPD_eq_slice {E : Type u_1} [AddCommGroup E] [Module ℝ E] (P D : Set E) : {x : E | (1, x) ∈ ↑(PointedCone.hull ℝ (liftPD P D))} = convexHullPD P D

The homogenisation dictionary. conv S is the level-one slice of the convex cone in ℝ × E generated by liftPD P D, the copy of P at height 1 together with the copy of D at height 0. This is Rockafellar's S', and the identification is what carries almost every proof about conv S.

theorem Tdaf.ConvexAnalysis.mem_convexHullPD_iff_lift_mem {E : Type u_1} [AddCommGroup E] [Module ℝ E] {P D : Set E} {x : E} : x ∈ convexHullPD P D ↔ (1, x) ∈ ↑(PointedCone.hull ℝ (liftPD P D))

The level-one slice form of membership in conv S.

Half-lines in a normed space

theorem Tdaf.ConvexAnalysis.not_isBounded_halfLine {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x y : E} (hy : y ≠ 0) : ¬Bornology.IsBounded (halfLine x y)

A half-line in a nonzero direction is unbounded.

Carathéodory's theorem, and closedness

theorem Tdaf.ConvexAnalysis.exists_of_mem_convexHullPD {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {P D : Set E} {x : E} (hx : x ∈ convexHullPD P D) : ∃ (p : Finset E) (d : Finset E) (a : E → ℝ) (b : E → ℝ), ↑p ⊆ P ∧ ↑d ⊆ D ∧ (∀ y ∈ p, 0 < a y) ∧ (∀ y ∈ d, 0 < b y) ∧ ∑ y ∈ p, a y = 1 ∧ p.card + d.card ≤ Module.finrank ℝ E + 1 ∧ ∑ y ∈ p, a y • y + ∑ y ∈ d, b y • y = x

Carathéodory's theorem for points and directions: every point of conv S is a convex combination of at most n + 1 points and directions of S, all with strictly positive coefficients.

theorem Tdaf.ConvexAnalysis.sum_mem_convexHullPD {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {P D : Set E} {p d : Finset E} {a b : E → ℝ} (hp : ↑p ⊆ P) (hd : ↑d ⊆ D) (ha : ∀ y ∈ p, 0 ≤ a y) (hb : ∀ y ∈ d, 0 ≤ b y) (hsum : ∑ y ∈ p, a y = 1) : ∑ y ∈ p, a y • y + ∑ y ∈ d, b y • y ∈ convexHullPD P D

The converse of exists_of_mem_convexHullPD: any convex combination of points and directions of S lies in conv S.

theorem Tdaf.ConvexAnalysis.IsCompact.isClosed_convexHullPD {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {P D : Set E} (hP : IsCompact P) (hD : IsClosed ↑(PointedCone.hull ℝ D)) : IsClosed (convexHullPD P D)

A closedness criterion. conv S is closed as soon as the set of points is compact and the cone generated by the directions is closed: the convex hull of a compact set is compact, and a compact set plus a closed set is closed.

theorem Tdaf.ConvexAnalysis.IsCompact.isCompact_convexHullPD {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {P : Set E} (hP : IsCompact P) : IsCompact (convexHullPD P ∅)

conv S is compact when there are no directions and the points are compact.

Vertices: affine independence, dimension, generalized simplices

theorem Tdaf.ConvexAnalysis.coe_coneHull_subset_span {E : Type u_1} [AddCommGroup E] [Module ℝ E] (S : Set E) : ↑(PointedCone.hull ℝ S) ⊆ ↑(Submodule.span ℝ S)

The pointed cone generated by a set lies inside its linear span.

def Tdaf.ConvexAnalysis.affineSpanPD {E : Type u_1} [AddCommGroup E] [Module ℝ E] (P D : Set E) : AffineSubspace ℝ E

The affine hull of a set of points and directions: aff S = aff (conv S), the smallest affine set containing the points of S that recedes in all the directions of S.

Equations

• Tdaf.ConvexAnalysis.affineSpanPD P D = affineSpan ℝ (Tdaf.ConvexAnalysis.convexHullPD P D)

noncomputable def Tdaf.ConvexAnalysis.finrankPD {E : Type u_1} [AddCommGroup E] [Module ℝ E] (P D : Set E) : ℕ

The dimension of a set of points and directions, dim S = dim (aff S), as the dimension of the direction space of aff S. Rockafellar gives the empty set dimension -1; a natural number cannot, so finrankPD ∅ D = 0 and every statement about it carries a non-emptiness hypothesis.

Equations

• Tdaf.ConvexAnalysis.finrankPD P D = Module.finrank ℝ ↥(vectorSpan ℝ (Tdaf.ConvexAnalysis.convexHullPD P D))

theorem Tdaf.ConvexAnalysis.finrankPD_def {E : Type u_1} [AddCommGroup E] [Module ℝ E] (P D : Set E) : finrankPD P D = Module.finrank ℝ ↥(vectorSpan ℝ (convexHullPD P D))

dim S unfolded.

theorem Tdaf.ConvexAnalysis.finrankPD_eq_finrank_direction {E : Type u_1} [AddCommGroup E] [Module ℝ E] (P D : Set E) : finrankPD P D = Module.finrank ℝ ↥(affineSpanPD P D).direction

dim S is the dimension of the direction space of aff S.

def Tdaf.ConvexAnalysis.AffineIndepPD {E : Type u_1} [AddCommGroup E] [Module ℝ E] (P D : Set E) : Prop

A set of points and directions is affinely independent when its homogenisation — the points lifted to height 1 and the directions to height 0 — is linearly independent in ℝ × E. Rockafellar defines the notion by dim S = m - 1 and derives this criterion; here the criterion is the definition. With no directions it is affine independence of the points.

Equations

• Tdaf.ConvexAnalysis.AffineIndepPD P D = LinearIndepOn ℝ id (Tdaf.ConvexAnalysis.liftPD P D)

theorem Tdaf.ConvexAnalysis.affineIndepPD_iff {E : Type u_1} [AddCommGroup E] [Module ℝ E] {P D : Set E} : AffineIndepPD P D ↔ LinearIndepOn ℝ id (liftPD P D)

Affine independence of a mixed set, unfolded.

def Tdaf.ConvexAnalysis.IsSimplexPD {E : Type u_1} [AddCommGroup E] [Module ℝ E] (m : ℕ) (C : Set E) : Prop

A generalized m-dimensional simplex: the convex hull of m + 1 affinely independent points and directions. The points are its ordinary vertices and the directions its vertices at infinity; the one-dimensional ones are the line segments and the closed half-lines, and one with a single ordinary vertex is a skew orthant.

Equations

• Tdaf.ConvexAnalysis.IsSimplexPD m C = ∃ (p : Finset E) (d : Finset E), Tdaf.ConvexAnalysis.AffineIndepPD ↑p ↑d ∧ p.card + d.card = m + 1 ∧ C = Tdaf.ConvexAnalysis.convexHullPD ↑p ↑d

theorem Tdaf.ConvexAnalysis.isSimplexPD_convexHullPD {E : Type u_1} [AddCommGroup E] [Module ℝ E] {p d : Finset E} {m : ℕ} (hai : AffineIndepPD ↑p ↑d) (hcard : p.card + d.card = m + 1) : IsSimplexPD m (convexHullPD ↑p ↑d)

The convex hull of m + 1 affinely independent points and directions is a generalized m-dimensional simplex.

theorem Tdaf.ConvexAnalysis.ncard_liftPD_coe {E : Type u_1} (p d : Finset E) : (liftPD ↑p ↑d).ncard = p.card + d.card

The homogenisation of a finite set of points and a finite set of directions has exactly as many elements as there are points and directions: the heights 1 and 0 keep the two families apart, and each lift is injective.

conv S as a union of simplices

theorem Tdaf.ConvexAnalysis.finrank_span_liftPD {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {P D : Set E} (hP : P.Nonempty) : Module.finrank ℝ ↥(Submodule.span ℝ (liftPD P D)) = finrankPD P D + 1

The homogenisation raises the dimension by exactly one. When S has at least one point, the span of liftPD P D in ℝ × E has dimension dim S + 1 — Rockafellar's dim K = d + 1. Fixing x₀ ∈ S, that span is the direct sum of the line through (1, x₀) and the copy of the direction space of aff S at height 0.

theorem Tdaf.ConvexAnalysis.finrankPD_add_one_of_affineIndepPD {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {p d : Finset E} (hp : (↑p).Nonempty) (hai : AffineIndepPD ↑p ↑d) : finrankPD ↑p ↑d + 1 = p.card + d.card

A generalized m-dimensional simplex really has dimension m. Rockafellar defines affine independence of a mixed set by dim S = m - 1; this recovers that definition from the linear-independence criterion AffineIndepPD takes as primitive.

theorem Tdaf.ConvexAnalysis.finrank_vectorSpan_of_isSimplexPD {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {m : ℕ} {C : Set E} (hC : IsSimplexPD m C) (hne : C.Nonempty) : Module.finrank ℝ ↥(vectorSpan ℝ C) = m

A generalized m-dimensional simplex has dimension m, in the form its name promises.

theorem Tdaf.ConvexAnalysis.convexHullPD_eq_iUnion_simplex {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {P D : Set E} (hP : P.Nonempty) : convexHullPD P D = ⋃ (p : Finset E), ⋃ (d : Finset E), ⋃ (_ : ↑p ⊆ P), ⋃ (_ : ↑d ⊆ D), ⋃ (_ : AffineIndepPD ↑p ↑d), ⋃ (_ : p.card + d.card = finrankPD P D + 1), convexHullPD ↑p ↑d

conv S is the union of all the generalized d-dimensional simplices whose vertices belong to S, where d = dim (conv S). Carathéodory produces an independent family of at most d + 1 generators; padding it to exactly d + 1 extends that family to a basis of the span of liftPD P D, drawing the extra vectors from liftPD P D itself — possible because that span has dimension exactly d + 1.