theorem exists_eq_image_add_smul_Ici_of_closedHalf_affine_finrank_one {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCne : C.Nonempty) (hfin : Module.finrank ℝ ↥(affineSpan ℝ C).direction = 1) (hNoLines : ¬∃ (y : EuclideanSpace ℝ (Fin n)), y ≠ 0 ∧ y ∈ -C.recessionCone ∩ C.recessionCone) (hHalf : ∃ (A : AffineSubspace ℝ (EuclideanSpace ℝ (Fin n))) (f : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] ℝ) (a : ℝ), f ≠ 0 ∧ C = ↑A ∩ {x : EuclideanSpace ℝ (Fin n) | f x ≤ a}) : ∃ (x0 : EuclideanSpace ℝ (Fin n)) (d : EuclideanSpace ℝ (Fin n)), d ≠ 0 ∧ C = (fun (t : ℝ) => x0 + t • d) '' Set.Ici 0

A closed half-affine set of affine direction finrank 1 is a ray.

theorem ray_subset_mixedConvexHull_of_closedHalf_affine_finrank_one {n : ℕ} {C : Set (Fin n → ℝ)} (hCconv : Convex ℝ C) (hNoLines : ¬∃ (y : Fin n → ℝ), y ≠ 0 ∧ y ∈ -C.recessionCone ∩ C.recessionCone) (hCne : C.Nonempty) (hfin : Module.finrank ℝ ↥(affineSpan ℝ C).direction = 1) (hHalf : ∃ (A : AffineSubspace ℝ (EuclideanSpace ℝ (Fin n))) (f : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] ℝ) (a : ℝ), f ≠ 0 ∧ ⇑(euclideanEquiv n).symm '' C = ↑A ∩ {x : EuclideanSpace ℝ (Fin n) | f x ≤ a}) : C ⊆ mixedConvexHull (Set.extremePoints ℝ C) {d : Fin n → ℝ | IsExtremeDirection C d}

In the closed-half-affine finrank-one case, every point lies in the mixed convex hull.

theorem closedConvex_eq_mixedConvexHull_of_finrank_direction_eq_one {n : ℕ} {C : Set (Fin n → ℝ)} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hNoLines : ¬∃ (y : Fin n → ℝ), y ≠ 0 ∧ y ∈ -C.recessionCone ∩ C.recessionCone) (hfin : Module.finrank ℝ ↥(affineSpan ℝ C).direction = 1) : C = mixedConvexHull (Set.extremePoints ℝ C) {d : Fin n → ℝ | IsExtremeDirection C d}

Base case: one-dimensional closed convex sets without lines are generated by extreme points and directions.

theorem not_affine_or_closedHalf_of_noLines_finrank_gt_one {n : ℕ} {C : Set (Fin n → ℝ)} (hNoLines : ¬∃ (y : Fin n → ℝ), y ≠ 0 ∧ y ∈ -C.recessionCone ∩ C.recessionCone) (hfin : 1 < Module.finrank ℝ ↥(affineSpan ℝ C).direction) : (¬∃ (A : AffineSubspace ℝ (EuclideanSpace ℝ (Fin n))), ↑A = ⇑(euclideanEquiv n).symm '' C) ∧ ¬∃ (A : AffineSubspace ℝ (EuclideanSpace ℝ (Fin n))) (f : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] ℝ) (a : ℝ), f ≠ 0 ∧ ⇑(euclideanEquiv n).symm '' C = ↑A ∩ {x : EuclideanSpace ℝ (Fin n) | f x ≤ a}

In dimension > 1, a closed convex set with no lines is neither affine nor a closed half of an affine set.

theorem closedConvex_subset_mixedConvexHull_by_finrank_strongInduction {n : ℕ} {C : Set (Fin n → ℝ)} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hNoLines : ¬∃ (y : Fin n → ℝ), y ≠ 0 ∧ y ∈ -C.recessionCone ∩ C.recessionCone) (hCne : C.Nonempty) : C ⊆ mixedConvexHull (Set.extremePoints ℝ C) {d : Fin n → ℝ | IsExtremeDirection C d}

Strong induction on finrank of the affine span direction to show C ⊆ mixedConvexHull.

theorem closedConvex_eq_mixedConvexHull_extremePoints_extremeDirections {n : ℕ} (C : Set (Fin n → ℝ)) (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hNoLines : ¬∃ (y : Fin n → ℝ), y ≠ 0 ∧ y ∈ -C.recessionCone ∩ C.recessionCone) : C = mixedConvexHull (Set.extremePoints ℝ C) {d : Fin n → ℝ | IsExtremeDirection C d}

Theorem 18.5. Let C be a closed convex set containing no lines, and let S be the set of all extreme points and extreme directions of C. Then C = conv S.

Here we formalize conv S as the mixed convex hull mixedConvexHull S₀ S₁ (Definition 17.0.4), with S₀ = C.extremePoints ℝ and S₁ = {d | IsExtremeDirection (𝕜 := ℝ) C d}.

theorem hRegular_to_hNoUnbounded_for_mixedConvexHull {n : ℕ} {S₀ S₁ : Set (Fin n → ℝ)} (hRegular : ∀ (x d' : Fin n → ℝ), Bornology.IsBounded (S₀ ∩ (fun (t : ℝ) => x + t • d') '' Set.Ici 0)) (x d' : Fin n → ℝ) : (fun (t : ℝ) => x + t • d') '' Set.Ici 0 ⊆ mixedConvexHull S₀ S₁ → Bornology.IsBounded (S₀ ∩ (fun (t : ℝ) => x + t • d') '' Set.Ici 0)

Regularity along all rays implies the boundedness condition used for mixed convex hulls.

theorem extremePoints_subset_S0_of_eq_mixedConvexHull {n : ℕ} {C S₀ S₁ : Set (Fin n → ℝ)} (hCgen : C = mixedConvexHull S₀ S₁) : Set.extremePoints ℝ C ⊆ S₀

Extreme points of a mixed convex hull lie in the point-generators.

theorem extremePoints_subset_points_and_extremeDirections_subset_directions_of_eq_mixedConvexHull {n : ℕ} {C : Set (Fin n → ℝ)} (S₀ S₁ : Set (Fin n → ℝ)) (hCgen : C = mixedConvexHull S₀ S₁) (hRegular : ∀ (x d' : Fin n → ℝ), Bornology.IsBounded (S₀ ∩ (fun (t : ℝ) => x + t • d') '' Set.Ici 0)) : Set.extremePoints ℝ C ⊆ S₀ ∧ {d : Fin n → ℝ | IsExtremeDirection C d} ⊆ rayNonneg n S₁

Text 18.5.1 (Minimality of Extreme Elements). Let C be a closed convex set containing no lines. Let S be the set of all extreme points and extreme directions of C.

Suppose S' is another set of point-elements and direction-elements such that:

(1) C is fully generated by S', i.e. C = conv(S') (here formalized as a mixed convex hull mixedConvexHull S₀ S₁).

(2) (Regularity condition) No half-line in ℝⁿ contains an unbounded subset of the point-elements of S' (here: the intersection of S₀ with any ray is bounded).

Then S ⊆ S' (here: every extreme point belongs to S₀, and every extreme direction belongs to S₁).

theorem recessionCone_eq_singleton_zero_of_closed_bounded_convex_fin {n : ℕ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hCbdd : Bornology.IsBounded C) : C.recessionCone = {0}

Bounded closed convex sets have trivial recession cone in Fin n → ℝ.

theorem noLines_of_recessionCone_eq_singleton_zero {n : ℕ} {C : Set (Fin n → ℝ)} (hrec : C.recessionCone = {0}) : ¬∃ (y : Fin n → ℝ), y ≠ 0 ∧ y ∈ -C.recessionCone ∩ C.recessionCone

If the recession cone is {0}, then C contains no lines.

theorem extremeDirections_eq_empty_of_recessionCone_eq_singleton_zero {n : ℕ} {C : Set (Fin n → ℝ)} (hCclosed : IsClosed C) (hrec : C.recessionCone = {0}) : {d : Fin n → ℝ | IsExtremeDirection C d} = ∅

If the recession cone is {0}, then C has no extreme directions.

theorem mixedConvexHull_empty_directions_eq_convexHull {n : ℕ} (S₀ : Set (Fin n → ℝ)) : mixedConvexHull S₀ ∅ = (convexHull ℝ) S₀

Mixed convex hull with empty directions reduces to the usual convex hull.