theorem closed_bounded_convex_eq_convexHull_extremePoints_part9 {n : ℕ} (C : Set (Fin n → ℝ)) (hCclosed : IsClosed C) (hCbounded : Bornology.IsBounded C) (hCconv : Convex ℝ C) : C = (convexHull ℝ) (Set.extremePoints ℝ C)

Corollary 18.5.1. Let C be a closed bounded convex set. Then C is the convex hull of its extreme points.

theorem theorem18_6_isExtremePoint_mono {n : ℕ} {C D : Set (Fin n → ℝ)} {x : Fin n → ℝ} (hDC : D ⊆ C) (hxD : x ∈ D) (hxext : IsExtremePoint C x) : IsExtremePoint D x

Extreme points are monotone with respect to set inclusion.

theorem theorem18_6_isClosed_conv_closure_exposedPoints {n : ℕ} {C : Set (Fin n → ℝ)} (hCclosed : IsClosed C) (hCbounded : Bornology.IsBounded C) (hCconv : Convex ℝ C) : IsClosed (conv (closure (Set.exposedPoints ℝ C))) ∧ conv (closure (Set.exposedPoints ℝ C)) ⊆ C

conv (closure (exposedPoints)) is closed and contained in the set.

theorem theorem18_6_not_mem_C0_of_extreme_not_mem_closure_exposedPoints {n : ℕ} {C : Set (Fin n → ℝ)} (hCclosed : IsClosed C) (hCbounded : Bornology.IsBounded C) (hCconv : Convex ℝ C) {x : Fin n → ℝ} (hxext : IsExtremePoint C x) (hxnot : x ∉ closure (Set.exposedPoints ℝ C)) : x ∉ conv (closure (Set.exposedPoints ℝ C))

An extreme point outside the closure of exposed points is not in conv (closure ...).

theorem theorem18_6_exists_exposedFace_disjoint_closedConvex {n : ℕ} {C D : Set (Fin n → ℝ)} (hCcompact : IsCompact C) (hDclosed : IsClosed D) (hDconv : Convex ℝ D) {x : Fin n → ℝ} (hxC : x ∈ C) (hxnotD : x ∉ D) : ∃ (l : (Fin n → ℝ) →L[ℝ] ℝ), (l.toExposed C).Nonempty ∧ IsExposed ℝ C (l.toExposed C) ∧ l.toExposed C ⊆ C \ D

Given a compact convex set C, a closed convex subset D, and a point x ∈ C \ D, there is a nonempty exposed face of C disjoint from D.

theorem theorem18_6_exists_exposedFace_disjoint_C0 {n : ℕ} {C : Set (Fin n → ℝ)} (hCclosed : IsClosed C) (hCbounded : Bornology.IsBounded C) (hCconv : Convex ℝ C) {x : Fin n → ℝ} (hxext : IsExtremePoint C x) (hxnot : x ∉ closure (Set.exposedPoints ℝ C)) : ∃ (l : (Fin n → ℝ) →L[ℝ] ℝ), (l.toExposed C).Nonempty ∧ IsExposed ℝ C (l.toExposed C) ∧ l.toExposed C ⊆ C \ conv (closure (Set.exposedPoints ℝ C))

An extreme point outside the closure of exposed points yields a disjoint exposed face.

theorem theorem18_6_exposed_eq_toExposed {n : ℕ} {C F : Set (Fin n → ℝ)} (hFexposed : IsExposed ℝ C F) (hFne : F.Nonempty) : ∃ (l : (Fin n → ℝ) →L[ℝ] ℝ), F = l.toExposed C

A nonempty exposed subset is of the form l.toExposed C.

theorem theorem18_6_exposedPoint_of_exposed_singleton {n : ℕ} {C : Set (Fin n → ℝ)} {p : Fin n → ℝ} (hFexposed : IsExposed ℝ C {p}) : p ∈ Set.exposedPoints ℝ C

An exposed singleton yields an exposed point.

theorem theorem18_6_vectorSpan_toExposed_le_ker {n : ℕ} {A : Set (Fin n → ℝ)} (g : (Fin n → ℝ) →L[ℝ] ℝ) : vectorSpan ℝ (g.toExposed A) ≤ LinearMap.ker ↑g

The vector span of a maximizer set lies in the kernel of the functional.

theorem theorem18_6_singleton_of_finrank_vectorSpan_eq_zero {n : ℕ} {F : Set (Fin n → ℝ)} (hFne : F.Nonempty) (hfin : Module.finrank ℝ ↥(vectorSpan ℝ F) = 0) : ∃ (p : Fin n → ℝ), F = {p}

If vectorSpan has dimension zero, the set is a singleton.

theorem theorem18_6_mem_toExposed_iff_eq_of_mem {n : ℕ} {C : Set (Fin n → ℝ)} {l : (Fin n → ℝ) →L[ℝ] ℝ} {z x : Fin n → ℝ} (hz : z ∈ l.toExposed C) (hxC : x ∈ C) : x ∈ l.toExposed C ↔ l x = l z

Relative to a fixed maximizer z, membership in l.toExposed C is equivalent to equality of functional values.

theorem theorem18_6_not_mem_toExposed_iff_lt_of_mem {n : ℕ} {C : Set (Fin n → ℝ)} {l : (Fin n → ℝ) →L[ℝ] ℝ} {z x : Fin n → ℝ} (hz : z ∈ l.toExposed C) (hxC : x ∈ C) : x ∉ l.toExposed C ↔ l x < l z

Relative to a fixed maximizer z, non-membership in l.toExposed C is equivalent to strict functional decrease.

theorem theorem18_6_toExposed_eq_levelset_of_mem {n : ℕ} {C : Set (Fin n → ℝ)} {l : (Fin n → ℝ) →L[ℝ] ℝ} {z : Fin n → ℝ} (hz : z ∈ l.toExposed C) : l.toExposed C = {x : Fin n → ℝ | x ∈ C ∧ l x = l z}

Any nonempty toExposed set is a level set in C at its maximizing value.

theorem theorem18_6_toExposed_subset_of_small_perturbation_of_uniform_gap {n : ℕ} {C : Set (Fin n → ℝ)} {l g : (Fin n → ℝ) →L[ℝ] ℝ} {z : Fin n → ℝ} (hz : z ∈ l.toExposed C) (hB : ∃ (B : ℝ), 0 ≤ B ∧ ∀ x ∈ C, |g x| ≤ B) (hgap : ∃ (δ : ℝ), 0 < δ ∧ ∀ y ∈ C \ l.toExposed C, l y ≤ l z - δ) : ∃ (ε : ℝ), 0 < ε ∧ (l + ε • g).toExposed C ⊆ l.toExposed C

Uniform-gap perturbation: if l has a positive gap away from l.toExposed C and g is bounded on C, then for small positive ε, every maximizer of l + ε g lies in l.toExposed C.

theorem theorem18_6_exists_uniform_gap_on_closed_disjoint_subset {n : ℕ} {C : Set (Fin n → ℝ)} (hCcompact : IsCompact C) {l : (Fin n → ℝ) →L[ℝ] ℝ} {z : Fin n → ℝ} (hz : z ∈ l.toExposed C) {K : Set (Fin n → ℝ)} (hKclosed : IsClosed K) (hKsub : K ⊆ C) (hKdisj : Disjoint K (l.toExposed C)) : ∃ (δ : ℝ), 0 < δ ∧ ∀ y ∈ K, l y ≤ l z - δ

On any closed subset of C disjoint from l.toExposed C, the exposing functional is uniformly below its maximal value by a positive gap.

theorem theorem18_6_compact_lexicographic_perturbation_singleton {n : ℕ} {C : Set (Fin n → ℝ)} {l g : (Fin n → ℝ) →L[ℝ] ℝ} {z : Fin n → ℝ} (hz : z ∈ l.toExposed C) (huniq : g.toExposed (l.toExposed C) = {z}) (hB : ∃ (B : ℝ), 0 ≤ B ∧ ∀ x ∈ C, |g x| ≤ B) (hgap : ∃ (δ : ℝ), 0 < δ ∧ ∀ y ∈ C \ l.toExposed C, l y ≤ l z - δ) : ∃ (ε : ℝ), 0 < ε ∧ (l + ε • g).toExposed C = {z}

Compact lexicographic perturbation (singleton target): if z is the unique g-maximizer on l.toExposed C and l has a uniform positive gap away from l.toExposed C, then for a small positive perturbation l + ε g, the exposed set on C is exactly {z}.

theorem theorem18_6_compact_lexicographic_perturbation_toExposed_eq {n : ℕ} {C : Set (Fin n → ℝ)} {l g : (Fin n → ℝ) →L[ℝ] ℝ} {z : Fin n → ℝ} (hz : z ∈ l.toExposed C) (hB : ∃ (B : ℝ), 0 ≤ B ∧ ∀ x ∈ C, |g x| ≤ B) (hgap : ∃ (δ : ℝ), 0 < δ ∧ ∀ y ∈ C \ l.toExposed C, l y ≤ l z - δ) : ∃ (ε : ℝ), 0 < ε ∧ (l + ε • g).toExposed C = g.toExposed (l.toExposed C)

Quantitative lexicographic perturbation: with a uniform gap away from l.toExposed C and a bound on g over C, a small perturbation realizes exactly g.toExposed (l.toExposed C).

theorem theorem18_6_exposedFace_contains_extremePoint_fin {n : ℕ} {C : Set (Fin n → ℝ)} (hCcompact : IsCompact C) {F : Set (Fin n → ℝ)} (hFexposed : IsExposed ℝ C F) (hFne : F.Nonempty) : ∃ p ∈ F, p ∈ Set.extremePoints ℝ C

A nonempty exposed face of a compact set contains an extreme point of the ambient set.

theorem theorem18_6_exposedPoint_of_compact_lexicographic_bridge {n : ℕ} {C : Set (Fin n → ℝ)} {l g : (Fin n → ℝ) →L[ℝ] ℝ} {z : Fin n → ℝ} (hz : z ∈ l.toExposed C) (huniq : g.toExposed (l.toExposed C) = {z}) (hB : ∃ (B : ℝ), 0 ≤ B ∧ ∀ x ∈ C, |g x| ≤ B) (hgap : ∃ (δ : ℝ), 0 < δ ∧ ∀ y ∈ C \ l.toExposed C, l y ≤ l z - δ) : z ∈ Set.exposedPoints ℝ C

Bridge-to-ambient step: once the compact lexicographic singleton data is available on an exposed face l.toExposed C, the selected point is an exposed point of C.

theorem theorem18_6_bridge_of_perturbation_limit {n : ℕ} {C : Set (Fin n → ℝ)} {l g : (Fin n → ℝ) →L[ℝ] ℝ} {ε : ℕ → ℝ} {p : ℕ → Fin n → ℝ} {z : Fin n → ℝ} (hzC : z ∈ C) (hpExp : ∀ (k : ℕ), p k ∈ Set.exposedPoints ℝ C) (hpPert : ∀ (k : ℕ), p k ∈ (l + ε k • g).toExposed C) (hpTend : Filter.Tendsto p Filter.atTop (nhds z)) (hεgP : Filter.Tendsto (fun (k : ℕ) => ε k * g (p k)) Filter.atTop (nhds 0)) (hεgConst : ∀ y ∈ C, Filter.Tendsto (fun (k : ℕ) => ε k * g y) Filter.atTop (nhds 0)) : ∃ q ∈ l.toExposed C, q ∈ closure (Set.exposedPoints ℝ C)

Perturbation-limit bridge: if exposed points p k are selected from perturbed maximizer sets (l + εₖ g).toExposed C, converge to z, and the perturbation terms vanish in the limit, then z lies in the exposed face l.toExposed C and in closure (C.exposedPoints ℝ).

theorem theorem18_6_compact_extract_subseq_exposed_perturbed {n : ℕ} {C : Set (Fin n → ℝ)} (hCcompact : IsCompact C) {l g : (Fin n → ℝ) →L[ℝ] ℝ} {ε : ℕ → ℝ} {p : ℕ → Fin n → ℝ} (hpExp : ∀ (k : ℕ), p k ∈ Set.exposedPoints ℝ C) (hpPert : ∀ (k : ℕ), p k ∈ (l + ε k • g).toExposed C) : ∃ z ∈ C, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Filter.Tendsto (fun (k : ℕ) => p (φ k)) Filter.atTop (nhds z) ∧ (∀ (k : ℕ), p (φ k) ∈ Set.exposedPoints ℝ C) ∧ ∀ (k : ℕ), p (φ k) ∈ (l + ε (φ k) • g).toExposed C

Compact extraction for perturbed exposed selectors.

theorem theorem18_6_perturbation_terms_tendsto_zero {n : ℕ} {C : Set (Fin n → ℝ)} {g : (Fin n → ℝ) →L[ℝ] ℝ} {ε : ℕ → ℝ} {p : ℕ → Fin n → ℝ} (hε : Filter.Tendsto ε Filter.atTop (nhds 0)) (hB : ∃ (B : ℝ), 0 ≤ B ∧ ∀ x ∈ C, |g x| ≤ B) (hpC : ∀ (k : ℕ), p k ∈ C) : Filter.Tendsto (fun (k : ℕ) => ε k * g (p k)) Filter.atTop (nhds 0) ∧ ∀ y ∈ C, Filter.Tendsto (fun (k : ℕ) => ε k * g y) Filter.atTop (nhds 0)

Vanishing perturbation terms from a vanishing scale and bounded functional values on C.

theorem theorem18_6_exists_abs_bound_on_compact {n : ℕ} {C : Set (Fin n → ℝ)} (hCcompact : IsCompact C) (g : (Fin n → ℝ) →L[ℝ] ℝ) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ x ∈ C, |g x| ≤ B

A continuous linear functional is uniformly bounded in absolute value on a compact set.

theorem theorem18_6_choose_selector_of_nonempty_intersections {n : ℕ} {C : Set (Fin n → ℝ)} {l g : (Fin n → ℝ) →L[ℝ] ℝ} (hNonempty : ∀ (k : ℕ), (Set.exposedPoints ℝ C ∩ (l + (1 / (↑k + 1)) • g).toExposed C).Nonempty) : ∃ (p : ℕ → Fin n → ℝ), (∀ (k : ℕ), p k ∈ Set.exposedPoints ℝ C) ∧ ∀ (k : ℕ), p k ∈ (l + (1 / (↑k + 1)) • g).toExposed C

Choice form: nonempty intersections of exposed points with perturbed exposed faces give a selector sequence.

theorem theorem18_6_mem_exposedPoints_of_isMaxOn_dotProduct_sub_self {n : ℕ} {C : Set (Fin n → ℝ)} {y p : Fin n → ℝ} (hpC : p ∈ C) (hpmax : IsMaxOn (fun (z : Fin n → ℝ) => (z - y) ⬝ᵥ (z - y)) C p) : p ∈ Set.exposedPoints ℝ C

A Euclidean-farthest point from y in C is an exposed point of C.

theorem theorem18_6_extremePoints_subset_closure_exposedPoints {n : ℕ} (C : Set (Fin n → ℝ)) (hCclosed : IsClosed C) (hCbounded : Bornology.IsBounded C) (hCconv : Convex ℝ C) : Set.extremePoints ℝ C ⊆ closure (Set.exposedPoints ℝ C)

Theorem 18.6. Every extreme point lies in the closure of the exposed points (bounded case).

theorem theorem18_7_rhs_subset_C {n : ℕ} {C : Set (Fin n → ℝ)} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) : closure (mixedConvexHull (Set.exposedPoints ℝ C) {d : Fin n → ℝ | IsExtremeDirection C d}) ⊆ C

The RHS mixed convex hull is contained in the closed convex set.

theorem theorem18_7_mixedConvexHull_recedes {n : ℕ} {S₀ S₁ : Set (Fin n → ℝ)} {d : Fin n → ℝ} (hd : d ∈ S₁) {x : Fin n → ℝ} (hx : x ∈ mixedConvexHull S₀ S₁) {t : ℝ} (ht : 0 ≤ t) : x + t • d ∈ mixedConvexHull S₀ S₁

The mixed convex hull recedes in all directions in its direction set.

theorem theorem18_7_K_isClosed_isConvex {n : ℕ} {C : Set (Fin n → ℝ)} : IsClosed (closure (mixedConvexHull (Set.exposedPoints ℝ C) {d : Fin n → ℝ | IsExtremeDirection C d})) ∧ Convex ℝ (closure (mixedConvexHull (Set.exposedPoints ℝ C) {d : Fin n → ℝ | IsExtremeDirection C d}))

The closure mixed convex hull is closed and convex.

theorem theorem18_7_K_recedes_extremeDirections {n : ℕ} {C : Set (Fin n → ℝ)} {d : Fin n → ℝ} (hd : d ∈ {d : Fin n → ℝ | IsExtremeDirection C d}) {x : Fin n → ℝ} (hx : x ∈ closure (mixedConvexHull (Set.exposedPoints ℝ C) {d : Fin n → ℝ | IsExtremeDirection C d})) {t : ℝ} (ht : 0 ≤ t) : x + t • d ∈ closure (mixedConvexHull (Set.exposedPoints ℝ C) {d : Fin n → ℝ | IsExtremeDirection C d})

The closure mixed convex hull recedes along extreme directions.

theorem theorem18_7_closure_exposedPoints_subset_K {n : ℕ} {C : Set (Fin n → ℝ)} : closure (Set.exposedPoints ℝ C) ⊆ closure (mixedConvexHull (Set.exposedPoints ℝ C) {d : Fin n → ℝ | IsExtremeDirection C d})

Exposed points are contained in the mixed convex hull, hence their closure lies in K.

theorem theorem18_7_extremePoints_subset_K {n : ℕ} {C : Set (Fin n → ℝ)} (hCclosed : IsClosed C) (hCbounded : Bornology.IsBounded C) (hCconv : Convex ℝ C) : Set.extremePoints ℝ C ⊆ closure (mixedConvexHull (Set.exposedPoints ℝ C) {d : Fin n → ℝ | IsExtremeDirection C d})

Extreme points lie in the closure mixed convex hull (bounded Straszewicz step).

theorem theorem18_7_C_subset_K_via_theorem18_5 {n : ℕ} {C : Set (Fin n → ℝ)} (hCclosed : IsClosed C) (hCbounded : Bornology.IsBounded C) (hCconv : Convex ℝ C) (hNoLines : ¬∃ (y : Fin n → ℝ), y ≠ 0 ∧ y ∈ -C.recessionCone ∩ C.recessionCone) : C ⊆ closure (mixedConvexHull (Set.exposedPoints ℝ C) {d : Fin n → ℝ | IsExtremeDirection C d})

Use Theorem 18.5 to show C ⊆ K once extreme points lie in K.

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

Theorem 18.7. A closed bounded convex set with no lines is the closure of the mixed convex hull of its exposed points and extreme directions.

theorem cor18_7_1_bounded_cone_subset_singleton_zero {n : ℕ} {K : Set (Fin n → ℝ)} (hKcone : IsConeSet n K) (hKbounded : Bornology.IsBounded K) : K ⊆ {0}

A bounded cone contains only the origin.

theorem cor18_7_1_bounded_cone_eq_singleton_zero {n : ℕ} {K : Set (Fin n → ℝ)} (hKcone : IsConeSet n K) (hKbounded : Bornology.IsBounded K) (hK0 : 0 ∈ K) : K = {0}

A bounded cone containing the origin is {0}.

theorem corollary18_7_1_closedConvexCone_eq_closure_cone {n : ℕ} (K T : Set (Fin n → ℝ)) (hKcone : IsConeSet n K) (hKbounded : Bornology.IsBounded K) (hK0 : 0 ∈ K) (hTsub : T ⊆ K) : K = closure (cone n T)

Corollary 18.7.1 (bounded cone version).

noncomputable def dotProductCLM {n : ℕ} (xStar : Fin n → ℝ) : (Fin n → ℝ) →L[ℝ] ℝ

The continuous linear functional x ↦ dotProduct x xStar.

Equations

• dotProductCLM xStar = LinearMap.toContinuousLinearMap ((dotProductBilin ℝ ℝ).flip xStar)

@[simp]

theorem dotProductCLM_apply {n : ℕ} (xStar y : Fin n → ℝ) : (dotProductCLM xStar) y = y ⬝ᵥ xStar

theorem theorem18_8_bddAbove_image_dotProduct_of_isCompact {n : ℕ} {C : Set (Fin n → ℝ)} (hCcompact : IsCompact C) (xStar : Fin n → ℝ) : BddAbove ((fun (y : Fin n → ℝ) => y ⬝ᵥ xStar) '' C)

A compact set gives a bounded-above dot-product image.

theorem theorem18_8_exists_exposedPoint_maximizer_dotProduct {n : ℕ} {C : Set (Fin n → ℝ)} (hCclosed : IsClosed C) (hCbounded : Bornology.IsBounded C) (hCne : C.Nonempty) (xStar : Fin n → ℝ) : ∃ p ∈ (dotProductCLM xStar).toExposed C, p ∈ Set.extremePoints ℝ C

For each xStar, there is an extreme-point maximizer of y ↦ dotProduct y xStar.

theorem theorem18_8_deltaStar_eq_dotProduct_of_mem_toExposed {n : ℕ} {C : Set (Fin n → ℝ)} (hCbd : ∀ (xStar : Fin n → ℝ), BddAbove ((fun (y : Fin n → ℝ) => y ⬝ᵥ xStar) '' C)) {xStar p : Fin n → ℝ} (hp : p ∈ (dotProductCLM xStar).toExposed C) : deltaStar C xStar = p ⬝ᵥ xStar

A maximizer in an exposed face realizes the support function value.

theorem theorem18_8_closedBoundedConvex_eq_sInter_tangentHalfspaces_exposedPoints {n : ℕ} (C : Set (Fin n → ℝ)) (hCclosed : IsClosed C) (hCbounded : Bornology.IsBounded C) (hCconv : Convex ℝ C) (hCne : C.Nonempty) : C = ⋂₀ {H : Set (Fin n → ℝ) | ∃ (xStar : Fin n → ℝ), ∃ p ∈ (dotProductCLM xStar).toExposed C, p ∈ Set.extremePoints ℝ C ∧ H = {x : Fin n → ℝ | x ⬝ᵥ xStar ≤ p ⬝ᵥ xStar}}

Theorem 18.8 (extreme-point form). A closed bounded convex set is the intersection of its tangent half-spaces at extreme points.