theorem positivelyHomogeneousConvexFunctionGenerated_convexHullFunction_eq_sInf_nonnegLinearCombination {n : ℕ} {f : (Fin n → ℝ) → EReal} (h_not_bot : ∀ (x : Fin n → ℝ), f x ≠ ⊥) (x : Fin n → ℝ) : x ≠ 0 → positivelyHomogeneousConvexFunctionGenerated (convexHullFunction f) x = sInf {z : EReal | ∃ (x' : Fin (n + 1) → Fin n → ℝ) (c : Fin (n + 1) → ℝ), (∀ (i : Fin (n + 1)), 0 ≤ c i) ∧ ∑ i : Fin (n + 1), c i • x' i = x ∧ z = ∑ i : Fin (n + 1), ↑(c i) * f (x' i)}

Corollary 17.1.6. Let f : ℝⁿ → (-∞, +∞] be any function (modeled here as f : (Fin n → ℝ) → EReal together with the side condition ∀ x, f x ≠ ⊥). Let k be the positively homogeneous convex function generated by f (equivalently, generated by conv f, modeled here as convexHullFunction f).

Then, for each vector x ≠ 0, k x = inf { ∑ i, λ i * f (xᵢ i) | ∑ i, λ i • xᵢ i = x }, where the infimum is taken over all expressions of x as a nonnegative linear combination of at most n+1 vectors (allowing zero coefficients to pad the representation).

theorem linearIndependent_lift1_of_affineIndependent {n d : ℕ} {p : Fin (d + 1) → Fin n → ℝ} (hp : AffineIndependent ℝ p) : LinearIndependent ℝ fun (i : Fin (d + 1)) (i_1 : Fin (n + 1)) => Fin.cases 1 (p i) i_1

Linear independence of the lifted points (1, p i) from affine independence of p.

theorem isGeneralizedSimplex_conv_range_of_affineIndependent {n d : ℕ} {p : Fin (d + 1) → Fin n → ℝ} (hp : AffineIndependent ℝ p) : IsGeneralizedSimplex n d (conv (Set.range p))

Convex hull of affinely independent vertices is a generalized simplex.

theorem exists_affineIndependent_vertices_through_point_finrank_direction {n : ℕ} {C : Set (Fin n → ℝ)} {x : Fin n → ℝ} (hx : x ∈ C) : have d := Module.finrank ℝ ↥(affineSpan ℝ C).direction; ∃ (p : Fin (d + 1) → Fin n → ℝ), p 0 = x ∧ (∀ (i : Fin (d + 1)), p i ∈ C) ∧ AffineIndependent ℝ p

For any x ∈ C, there are d+1 affinely independent points of C with x as the first vertex, where d is the finrank of the direction of affineSpan ℝ C.

theorem mixedConvexHull_eq_sUnion_generalizedSimplex_finrank_affineSpan_direction {n : ℕ} (S₀ S₁ : Set (Fin n → ℝ)) : have C := mixedConvexHull S₀ S₁; have d := Module.finrank ℝ ↥(affineSpan ℝ C).direction; C = ⋃₀ {T : Set (Fin n → ℝ) | IsGeneralizedSimplex n d T ∧ T ⊆ C}

Theorem 17.1 (Caratheodory's Theorem), union-of-simplices formulation. With C := mixedConvexHull S₀ S₁ and d := dim C (here d := finrank (affineSpan ℝ C).direction), the set C is the union of all generalized d-dimensional simplices contained in C.

theorem cor1717_isClosed_xAxis_union_point : IsClosed (cor1717_xAxis✝ ∪ {cor1717_p✝})

The x-axis union the point (0,1) is closed in Fin 2 → ℝ.

theorem cor1717_zSeq_mem_conv (k : ℕ) : cor1717_z✝ k ∈ conv (cor1717_xAxis✝ ∪ {cor1717_p✝})

The explicit convex-combination sequence lies in the convex hull.

theorem cor1717_tendsto_zSeq : Filter.Tendsto cor1717_z✝ Filter.atTop (nhds cor1717_lim✝)

The explicit sequence converges to (1,1).

theorem cor1717_limit_not_mem_conv : cor1717_lim✝ ∉ conv (cor1717_xAxis✝ ∪ {cor1717_p✝})

The limit point (1,1) is not in the convex hull of the x-axis union (0,1).

theorem exists_isClosed_set_conv_not_isClosed : ∃ (n : ℕ) (S : Set (Fin n → ℝ)), IsClosed S ∧ ¬IsClosed (conv S)

Crollary 17.1.7 (Convex hull of a closed set need not be closed), LaTeX label cor:conv-closed-not-closed.

In general, the convex hull of a closed subset of ℝⁿ need not be closed. In particular, if S ⊆ ℝ² is the union of a line and a single point not on that line, then conv(S) is not closed.

theorem cor1717_not_isClosed_conv_xAxis_union_point : ¬IsClosed (conv (cor1717_xAxis✝ ∪ {cor1717_p✝}))

The convex hull of the x-axis union (0,1) is not closed.

theorem exists_affineEquiv_image_line_eq_xAxis_and_map_point {L : AffineSubspace ℝ (Fin 2 → ℝ)} {p : Fin 2 → ℝ} (hL : Module.finrank ℝ ↥L.direction = 1) (hp : p ∉ ↑L) : ∃ (e : (Fin 2 → ℝ) ≃ᵃ[ℝ] Fin 2 → ℝ), ⇑e '' ↑L = cor1717_xAxis✝ ∧ e p = cor1717_p✝

An affine equivalence sending an affine line to the x-axis and a point off the line to (0,1).

theorem not_isClosed_conv_line_union_singleton {L : AffineSubspace ℝ (Fin 2 → ℝ)} {p : Fin 2 → ℝ} (hL : Module.finrank ℝ ↥L.direction = 1) (hp : p ∉ ↑L) : ¬IsClosed (conv (↑L ∪ {p}))

Crollary 17.1.7 (Convex hull of a closed set need not be closed), particular case: if S is the union of an affine line in ℝ² and a point not on that line, then conv(S) is not closed.

theorem isConvexWeights_iff_mem_stdSimplex {m : ℕ} {w : Fin m → ℝ} : IsConvexWeights m w ↔ w ∈ stdSimplex ℝ (Fin m)

Convex weights are exactly points in the standard simplex.

def convexCombinationSet {n : ℕ} (S : Set (Fin n → ℝ)) (m : ℕ) : Set (Fin n → ℝ)

The set of convex combinations of m points from closure S.

Equations

• convexCombinationSet S m = {y : Fin n → ℝ | ∃ (x : Fin m → ↑(closure S)) (w : Fin m → ℝ), IsConvexWeights m w ∧ y = convexCombination n m (fun (i : Fin m) => ↑(x i)) w}

theorem isCompact_convexCombinationSet_of_isCompact {n m : ℕ} {S : Set (Fin n → ℝ)} (hS : IsCompact (closure S)) : IsCompact (convexCombinationSet S m)

The m-point convex-combination set is compact when closure S is compact.

theorem conv_closure_eq_iUnion_convexCombinationSet {n : ℕ} (S : Set (Fin n → ℝ)) : conv (closure S) = ⋃ (m : Fin (n + 2)), convexCombinationSet S ↑m

Carathéodory-style union: conv (closure S) is the union of m-point combination sets.

theorem thm172_conv_closure_subset_closure_conv {n : ℕ} {S : Set (Fin n → ℝ)} : conv (closure S) ⊆ closure (conv S)

The easy inclusion conv (closure S) ⊆ closure (conv S).

theorem thm172_isClosed_conv_closure_of_isBounded {n : ℕ} {S : Set (Fin n → ℝ)} (hS : Bornology.IsBounded S) : IsClosed (conv (closure S))

Boundedness yields closedness of conv (closure S).

theorem thm172_closure_conv_subset_conv_closure_of_isBounded {n : ℕ} {S : Set (Fin n → ℝ)} (hS : Bornology.IsBounded S) : closure (conv S) ⊆ conv (closure S)

The bounded inclusion closure (conv S) ⊆ conv (closure S).

theorem closure_conv_eq_conv_closure_of_isBounded {n : ℕ} {S : Set (Fin n → ℝ)} (hS : Bornology.IsBounded S) : closure (conv S) = conv (closure S)

Theorem 17.2. If S is a bounded set of points in ℝⁿ, then closure (conv S) = conv (closure S). In particular, if S is closed and bounded, then conv S is closed and bounded.

theorem isClosed_and_isBounded_conv_of_isClosed_and_isBounded {n : ℕ} {S : Set (Fin n → ℝ)} (hS_closed : IsClosed S) (hS_bdd : Bornology.IsBounded S) : IsClosed (conv S) ∧ Bornology.IsBounded (conv S)

Theorem 17.2 (in particular). If S is closed and bounded, then conv S is closed and bounded.

theorem cor1721_isCompact_S {n : ℕ} {S : Set (Fin n → ℝ)} (hS_closed : IsClosed S) (hS_bdd : Bornology.IsBounded S) : IsCompact S

Compactness of a closed bounded subset of ℝⁿ.

theorem cor1721_exists_lowerBound_on_S {n : ℕ} {S : Set (Fin n → ℝ)} (hS_compact : IsCompact S) (hS_ne : S.Nonempty) {f : (Fin n → ℝ) → ℝ} (hf : ContinuousOn f S) : ∃ (m : ℝ), ∀ x ∈ S, m ≤ f x

A continuous function on a nonempty compact set is bounded below.

theorem cor1721_properConvexFunctionOn_convexHullFunction_fExt {n : ℕ} {S : Set (Fin n → ℝ)} (hS_ne : S.Nonempty) {f : (Fin n → ℝ) → ℝ} {m : ℝ} (hm : ∀ x ∈ S, m ≤ f x) : have fExt := fun (x : Fin n → ℝ) => ↑(f x) + indicatorFunction S x; ProperConvexFunctionOn Set.univ (convexHullFunction fExt)

Properness of convexHullFunction from a global lower bound on f over S.

theorem cor1721_fExt_ne_bot {n : ℕ} {S : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ} : have fExt := fun (x : Fin n → ℝ) => ↑(f x) + indicatorFunction S x; ∀ (x : Fin n → ℝ), fExt x ≠ ⊥

The extension fExt never takes the value ⊥.

theorem cor1721_isCompact_graph {n : ℕ} {S : Set (Fin n → ℝ)} (hS : IsCompact S) {f : (Fin n → ℝ) → ℝ} (hf : ContinuousOn f S) : IsCompact ((fun (x : Fin n → ℝ) => (x, f x)) '' S)

The graph of f over a compact set is compact.

theorem cor1721_isCompact_convexHull_graph {n : ℕ} {S : Set (Fin n → ℝ)} (hS_closed : IsClosed S) (hS_bdd : Bornology.IsBounded S) {f : (Fin n → ℝ) → ℝ} (hf : ContinuousOn f S) : have F := (fun (x : Fin n → ℝ) => (x, f x)) '' S; IsCompact ((convexHull ℝ) F)

The convex hull of the graph is compact in ℝ^{n+1}.

theorem cor1721_isClosed_K_add_convexHull_graph {n : ℕ} {S : Set (Fin n → ℝ)} (hS_closed : IsClosed S) (hS_bdd : Bornology.IsBounded S) {f : (Fin n → ℝ) → ℝ} (hf : ContinuousOn f S) : have F := (fun (x : Fin n → ℝ) => (x, f x)) '' S; have K := {p : (Fin n → ℝ) × ℝ | p.1 = 0 ∧ 0 ≤ p.2}; IsClosed (K + (convexHull ℝ) F)

The Minkowski sum of the vertical ray and the convex hull of the graph is closed.

theorem cor1721_epigraph_eq_K_add_convexHull_graph {n : ℕ} {S : Set (Fin n → ℝ)} (hS_closed : IsClosed S) (hS_bdd : Bornology.IsBounded S) {f : (Fin n → ℝ) → ℝ} (hf : ContinuousOn f S) : have fExt := fun (x : Fin n → ℝ) => ↑(f x) + indicatorFunction S x; have F := (fun (x : Fin n → ℝ) => (x, f x)) '' S; have K := {p : (Fin n → ℝ) × ℝ | p.1 = 0 ∧ 0 ≤ p.2}; epigraph Set.univ (convexHullFunction fExt) = K + (convexHull ℝ) F

The epigraph of the convex hull function is K + convexHull(graph).

theorem cor1721_isClosed_epigraph_convexHullFunction_fExt {n : ℕ} {S : Set (Fin n → ℝ)} (hS_closed : IsClosed S) (hS_bdd : Bornology.IsBounded S) {f : (Fin n → ℝ) → ℝ} (hf : ContinuousOn f S) : have fExt := fun (x : Fin n → ℝ) => ↑(f x) + indicatorFunction S x; IsClosed (epigraph Set.univ (convexHullFunction fExt))

Closedness of the epigraph of the convex hull function for fExt.

theorem closedConvex_and_properConvexFunctionOn_convexHullFunction_of_continuousOn_closed_bounded {n : ℕ} {S : Set (Fin n → ℝ)} (hS_ne : S.Nonempty) (hS_closed : IsClosed S) (hS_bdd : Bornology.IsBounded S) {f : (Fin n → ℝ) → ℝ} (hf : ContinuousOn f S) : have fExt := fun (x : Fin n → ℝ) => ↑(f x) + indicatorFunction S x; ClosedConvexFunction (convexHullFunction fExt) ∧ ProperConvexFunctionOn Set.univ (convexHullFunction fExt)

Corollary 17.2.1. Let S be a nonempty closed bounded set in ℝⁿ. Let f be a continuous real-valued function on S, and extend it by f(x) = +∞ for x ∉ S. Then conv f (here: convexHullFunction applied to the extension) is a closed proper convex function.

noncomputable def supremumInnerSub {n : ℕ} (S : Set (Fin n → ℝ)) (f : ↑S → EReal) (z : Fin n → ℝ) : EReal

Definition 17.2.2 (A convex function defined as a supremum), LaTeX label def:h.

Let S ⊆ ℝⁿ and let f : S → (ℝ ∪ {+∞}) (modeled here as f : S → EReal). Define h : ℝⁿ → (ℝ ∪ {+∞}) by

h z = sup { ⟪z, x⟫ - f x | x ∈ S }.

In Fin n → ℝ, the inner product ⟪z, x⟫ is expressed as ∑ i, z i * x i.

Equations

• supremumInnerSub S f z = sSup (Set.range fun (x : ↑S) => ↑(∑ i : Fin n, z i * ↑x i) - f x)