Carathéodory: a fixed index, cones, and points with directions

Mathlib has Carathéodory's theorem in the form convexHull_eq_union: every point of convexHull 𝕜 s lies in the convex hull of an affinely independent finite subset. What it does not have is any of the three things the theory needs — that n + 1 points always suffice with a fixed index type; the conical form, for the cone generated by a set; and the fact that the convex hull of a compact set is compact.

Corollary 17.1.4 in [^1], and its companion 17.1.6, are false as printed and are not formalised. Both assert that the positively homogeneous convex function generated by conv {fᵢ} is computed by an infimum restricted to representations using at most n linearly independent vectors. On R¹ take f₁(y) = -y and f₂(y) = y: then conv {f₁, f₂} ≡ -∞, so the generated function is -∞ everywhere, while at x = 1 the only admissible representations use a single index and give the values -1 and 1. The elimination behind convFn_apply_affineIndependent is unavailable, because an affine dependency has coefficients summing to zero — so both signs carry a positive coefficient and the sign may be chosen by the cost — whereas a conical dependency may have all coefficients of one sign. The printed proof passes to "a minimal α' on the vertical line", which does not exist when the generated function is improper.

Main results

• mem_convexHull_iff_exists_fin_finrank_succ — Carathéodory's theorem for points: membership in convexHull ℝ S is a convex combination indexed by Fin (finrank ℝ E + 1).
• exists_linearIndepOn_of_mem_coneHull — Carathéodory for convex cones: a point of the cone generated by S is a positive combination of a linearly independent subset of S. This is the algebraic core, the part a classical proof runs in R^{n+1}. exists_card_le_finrank_of_mem_coneHull is the same with the count ≤ n.
• exists_linearIndepOn_of_mem_convexHull_add_coneHull — Carathéodory for points and directions: a point of conv P + cone D uses at most n + 1 generators in total, and their homogenisation is linearly independent. exists_of_mem_convexHull_add_coneHull forgets the independence, exists_linearIndepOn_subset_liftPD states it in the homogenised vocabulary, and exists_finset_liftPD_eq reads a finite subset of the homogenisation back as points and directions.
• lift_mem_coneHull_liftPD — the easy half of the homogenisation dictionary; it needs neither a norm nor finite dimension, and HullDirections.lean builds the converse half on it.
• IsCompact.isCompact_convexHull, Bornology.IsBounded.closure_convexHull — the convex hull of a compact set is compact, and cl (conv S) = conv (cl S) for bounded S.
• closedProperConvexFn_convHullFn_restrict — the convex hull of a function with compact graph is a closed proper convex function.
• exists_subset_linearIndepOn_of_sum, exists_subset_affineIndependent_of_sum — the indexed elimination step: a representation ∑ i ∈ t, w i • v i is thinned to a sub-index set on which the generators are linearly (resp. affinely) independent. The affine form carries a real cost ∑ i ∈ t, w i * c i which the thinning is not allowed to increase.
• exists_coalesced_sum — Rockafellar's coalescing step: generators drawn from the same member of a family of convex sets are merged into their center of mass.
• exists_affineIndependent_of_mem_convexHull_iUnion, exists_linearIndepOn_of_mem_coneHull_iUnion — the same counts for a union of convex sets, in the convex and the conical form; exists_affineIndependent_of_convFn_lt, convFn_apply_affineIndependent — the convex hull of a family of functions; convHullFn_apply_fin — the convex hull of a single function, on a fixed index.
• inequalitySet, inequalitySet_subset_halfSpace_iff — which closed half-spaces contain the solution set of a compact system of linear inequalities. The Lean statement carries 0 ∉ S, which the usual statement omits and which is not removable; see the counterexample there.

Implementation notes

The fixed index is what makes compactness available: with Fin (n+1), convexHull ℝ S is the image of a compact set under a continuous map, and compactness of the hull is one line. Carathéodory's affinely independent subset has at most n+1 elements, and padding it out to exactly n+1 is the only real work. The classical hypothesis for cl (conv S) = conv (cl S) is boundedness, which coincides with compactness of the closure only because the space is finite-dimensional. The conical Carathéodory is an explicit induction on a cardinality bound rather than on a minimal representation, and its conclusion asserts strict positivity of the coefficients, which is what lets t.card ≤ finrank be read off from linear independence and makes the split into points and directions lossless.

References

[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §17.

theorem Tdaf.ConvexAnalysis.sum_ite_lt {M : Type u_1} [AddCommMonoid M] {m N : ℕ} (h : m ≤ N) (g : Fin N → M) : (∑ i : Fin N, if ↑i < m then g i else 0) = ∑ j : Fin m, g (Fin.castLE h j)

A sum over Fin N of a family cut off after the first m indices is a sum over Fin m. This is the padding lemma behind mem_convexHull_iff_exists_fin_finrank_succ.

theorem Tdaf.ConvexAnalysis.mem_convexHull_iff_exists_fin_finrank_succ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {S : Set E} {x : E} : x ∈ (convexHull ℝ) S ↔ ∃ (w : Fin (Module.finrank ℝ E + 1) → ℝ) (z : Fin (Module.finrank ℝ E + 1) → E), (∀ (i : Fin (Module.finrank ℝ E + 1)), 0 ≤ w i) ∧ ∑ i : Fin (Module.finrank ℝ E + 1), w i = 1 ∧ (∀ (i : Fin (Module.finrank ℝ E + 1)), z i ∈ S) ∧ ∑ i : Fin (Module.finrank ℝ E + 1), w i • z i = x

Carathéodory's theorem for points: a point of convexHull ℝ S is a convex combination of finrank ℝ E + 1 points of S, indexed by a fixed type. Repetitions and zero weights are allowed, which is exactly what turns Carathéodory's "at most n + 1 points" into a statement about a fixed index.

theorem Tdaf.ConvexAnalysis.IsCompact.isCompact_convexHull {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {S : Set E} (hS : IsCompact S) : IsCompact ((convexHull ℝ) S)

The convex hull of a compact set is compact: it is the image of stdSimplex × Sⁿ⁺¹ under (w, z) ↦ ∑ wᵢ zᵢ. Mathlib has this only for finite sets (Set.Finite.isCompact_convexHull).

theorem Tdaf.ConvexAnalysis.Bornology.IsBounded.closure_convexHull {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {S : Set E} (hS : Bornology.IsBounded S) : closure ((convexHull ℝ) S) = (convexHull ℝ) (closure S)

For a bounded set the closure and the convex hull commute.

The convex hull of a function with compact graph

theorem Tdaf.ConvexAnalysis.isClosed_convexHull_epi_restrict {E : Type u_1} [NormedAddCommGroup E] {S : Set E} {g : E → ℝ} [NormedSpace ℝ E] [FiniteDimensional ℝ E] (hS : IsCompact S) (hg : ContinuousOn g S) : IsClosed ((convexHull ℝ) (epi (restrict S fun (x : E) => ↑(g x))))

The convex hull of the epigraph of a function with compact graph is closed. The graph is compact, so its convex hull is compact, and a compact set plus the closed vertical ray is closed.

theorem Tdaf.ConvexAnalysis.closedProperConvexFn_convHullFn_restrict {E : Type u_1} [NormedAddCommGroup E] {S : Set E} {g : E → ℝ} [NormedSpace ℝ E] [FiniteDimensional ℝ E] (hSne : S.Nonempty) (hS : IsCompact S) (hg : ContinuousOn g S) : ClosedProperConvexFn (convHullFn (restrict S fun (x : E) => ↑(g x)))

The convex hull of a function with compact graph is a closed proper convex function. For non-empty compact S and g continuous on S, extended by +∞, the graph G of g is compact, so conv G is compact; epi f = G + K for the upward vertical ray K, so conv (epi f) = conv G + K is closed and upward closed on each vertical line, hence is an epigraph.

Carathéodory for convex cones

theorem Tdaf.ConvexAnalysis.exists_linearIndepOn_of_mem_coneHull {E : Type u_1} [AddCommGroup E] [Module ℝ E] {S : Set E} {x : E} (hx : x ∈ PointedCone.hull ℝ S) : ∃ (t : Finset E) (w : E → ℝ), ↑t ⊆ S ∧ (∀ y ∈ t, 0 < w y) ∧ LinearIndepOn ℝ id ↑t ∧ ∑ y ∈ t, w y • y = x

Carathéodory's theorem for convex cones. A point of the cone generated by S is a non-negative combination of a linearly independent finite subset of S, with strictly positive coefficients. This is the algebraic core of Carathéodory's theorem — the part a classical proof carries out in R^{n+1} — and Mathlib covers only the convex hull.

theorem Tdaf.ConvexAnalysis.exists_card_le_finrank_of_mem_coneHull {E : Type u_1} [AddCommGroup E] [Module ℝ E] [FiniteDimensional ℝ E] {S : Set E} {x : E} (hx : x ∈ PointedCone.hull ℝ S) : ∃ (t : Finset E) (w : E → ℝ), ↑t ⊆ S ∧ (∀ y ∈ t, 0 < w y) ∧ t.card ≤ Module.finrank ℝ E ∧ ∑ y ∈ t, w y • y = x

The conical Carathéodory bound: n generators suffice, where n = dim E.

Carathéodory for points and directions

def Tdaf.ConvexAnalysis.liftPD {E : Type u_1} (P D : Set E) : Set (ℝ × E)

The homogenisation of a set of points and directions: P is lifted to height 1 and D to height 0 in ℝ × E. Rockafellar's S'.

Equations

• Tdaf.ConvexAnalysis.liftPD P D = (fun (y : E) => (1, y)) '' P ∪ (fun (y : E) => (0, y)) '' D

theorem Tdaf.ConvexAnalysis.mem_liftPD_one {E : Type u_1} {P D : Set E} {y : E} (hy : y ∈ P) : (1, y) ∈ liftPD P D

A point of P sits at height 1 in liftPD P D.

theorem Tdaf.ConvexAnalysis.mem_liftPD_zero {E : Type u_1} {P D : Set E} {y : E} (hy : y ∈ D) : (0, y) ∈ liftPD P D

A direction of D sits at height 0 in liftPD P D.

theorem Tdaf.ConvexAnalysis.fst_eq_or_of_mem_liftPD {E : Type u_1} {P D : Set E} {q : ℝ × E} (hq : q ∈ liftPD P D) : q.1 = 1 ∨ q.1 = 0

Every element of liftPD P D sits at height 1 or at height 0.

theorem Tdaf.ConvexAnalysis.mem_of_mem_liftPD_of_fst_eq_one {E : Type u_1} {P D : Set E} {q : ℝ × E} (hq : q ∈ liftPD P D) (h1 : q.1 = 1) : q.2 ∈ P

An element of liftPD P D at height 1 is a point of P.

theorem Tdaf.ConvexAnalysis.mem_of_mem_liftPD_of_fst_eq_zero {E : Type u_1} {P D : Set E} {q : ℝ × E} (hq : q ∈ liftPD P D) (h0 : q.1 = 0) : q.2 ∈ D

An element of liftPD P D at height 0 is a direction of D.

theorem Tdaf.ConvexAnalysis.exists_finset_liftPD_eq {E : Type u_1} {P D : Set E} {t : Finset (ℝ × E)} (ht : ↑t ⊆ liftPD P D) : ∃ (p : Finset E) (d : Finset E), ↑p ⊆ P ∧ ↑d ⊆ D ∧ p.card + d.card = t.card ∧ liftPD ↑p ↑d = ↑t

Splitting a finite subset of the homogenisation. A finite set of vectors drawn from liftPD P D is itself the homogenisation of a finite set of points of P and a finite set of directions of D, with the two cardinalities adding up to its own.

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

The easy half of the homogenisation dictionary. A point of conv P + cone D, lifted to height 1, lies in the pointed cone generated by the homogenisation liftPD P D. It is stated on the unfolded conv P + cone D because convexHullPD P D, which is that expression by definition, is introduced above this file; the converse half is convexHullPD_eq_slice there.

theorem Tdaf.ConvexAnalysis.exists_linearIndepOn_subset_liftPD {E : Type u_1} [AddCommGroup E] [Module ℝ E] {P D : Set E} {x : E} (hx : x ∈ (convexHull ℝ) P + ↑(PointedCone.hull ℝ D)) : ∃ (t : Finset (ℝ × E)) (w : ℝ × E → ℝ), ↑t ⊆ liftPD P D ∧ (∀ q ∈ t, 0 < w q) ∧ LinearIndepOn ℝ id ↑t ∧ ∑ q ∈ t, w q • q = (1, x)

Carathéodory for points and directions, in homogenised form. A point of conv P + cone D lifts to (1, x), which is a positive combination of a linearly independent finite subset of the homogenisation liftPD P D. This is the form the theorem is proved in and the only one that keeps the linear independence.

theorem Tdaf.ConvexAnalysis.exists_linearIndepOn_of_mem_convexHull_add_coneHull {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {P D : Set E} {x : E} (hx : x ∈ (convexHull ℝ) P + ↑(PointedCone.hull ℝ 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 ∧ LinearIndepOn ℝ id (liftPD ↑p ↑d) ∧ ∑ y ∈ p, a y • y + ∑ y ∈ d, b y • y = x

Carathéodory for points and directions. A point of conv P + cone D is a convex combination of points of P plus a non-negative combination of directions of D, using at most n + 1 generators in total, n = dim E, all with strictly positive coefficients, and the generators so obtained are independent: their homogenisation liftPD ↑p ↑d is linearly independent in ℝ × E.

The proof homogenises to ℝ × E, where conv P + cone D is the level-one slice of the cone generated by {1} × P ∪ {0} × D, and applies the conical Carathéodory theorem there. Linear independence in ℝ × E is what produces the bound n + 1, and the first coordinate is what makes the point weights sum to 1. The independence clause is what the simplex form of the theorem needs, and it is not recoverable from exists_of_mem_convexHull_add_coneHull.

theorem Tdaf.ConvexAnalysis.exists_of_mem_convexHull_add_coneHull {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {P D : Set E} {x : E} (hx : x ∈ (convexHull ℝ) P + ↑(PointedCone.hull ℝ 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 for points and directions, with the independence of the generators forgotten. This is the form most consumers want; exists_linearIndepOn_of_mem_convexHull_add_coneHull keeps the independence as well.

Generators drawn from distinct members of a family

Corollaries 17.1.1–17.1.3 all sharpen Carathéodory's theorem by insisting that the generators come from different members of a family. The whole content is the elimination step below, run on an index set rather than on a set of vectors: a representation x = ∑ i ∈ t, w i • v i indexed by t : Finset ι already carries at most one generator per index, so no coalescing is needed after the fact.

theorem Tdaf.ConvexAnalysis.exists_pos_of_sum_eq_zero {ι : Type u_2} {s : Finset ι} {g : ι → ℝ} (hsum : ∑ i ∈ s, g i = 0) (hne : ∃ i ∈ s, g i ≠ 0) : ∃ i ∈ s, 0 < g i

A family of reals summing to zero over a Finset, not identically zero there, has a strictly positive member. This is what makes the sign of an affine dependency free to choose.

theorem Tdaf.ConvexAnalysis.exists_subset_linearIndepOn_of_sum {E : Type u_1} [AddCommGroup E] [Module ℝ E] {ι : Type u_2} (v : ι → E) (t : Finset ι) (w : ι → ℝ) (hw : ∀ i ∈ t, 0 < w i) : ∃ (t' : Finset ι) (w' : ι → ℝ), t' ⊆ t ∧ (∀ i ∈ t', 0 < w' i) ∧ LinearIndepOn ℝ v ↑t' ∧ ∑ i ∈ t', w' i • v i = ∑ i ∈ t, w i • v i

Carathéodory's elimination, indexed, conical form. A non-negative combination ∑ i ∈ t, w i • v i is thinned to a sub-index set on which the v i are linearly independent, keeping the value and strict positivity of the coefficients. Because the index set only shrinks, at most one generator is used per index — the "each belonging to a different Cᵢ" clause of the union form.

theorem Tdaf.ConvexAnalysis.card_le_finrank_of_linearIndepOn {E : Type u_1} [AddCommGroup E] [Module ℝ E] {ι : Type u_2} [FiniteDimensional ℝ E] {v : ι → E} {t : Finset ι} (h : LinearIndepOn ℝ v ↑t) : t.card ≤ Module.finrank ℝ E

Linear independence over an index set bounds the size of the index set by the dimension.

theorem Tdaf.ConvexAnalysis.affineIndependent_of_linearIndepOn_one {E : Type u_1} [AddCommGroup E] [Module ℝ E] {ι : Type u_2} {p : ι → E} {s : Set ι} (h : LinearIndepOn ℝ (fun (i : ι) => (1, p i)) s) : AffineIndependent ℝ fun (i : ↑s) => p ↑i

A linearly independent lift i ↦ (1, p i) is an affinely independent family i ↦ p i. This is the standard homogenisation, read on an index set.

theorem Tdaf.ConvexAnalysis.exists_subset_affineIndependent_of_sum {E : Type u_1} [AddCommGroup E] [Module ℝ E] {ι : Type u_2} (p : ι → E) (c : ι → ℝ) (t : Finset ι) (w : ι → ℝ) (hw : ∀ i ∈ t, 0 < w i) : ∃ (t' : Finset ι) (w' : ι → ℝ), t' ⊆ t ∧ (∀ i ∈ t', 0 < w' i) ∧ (AffineIndependent ℝ fun (i : ↑↑t') => p ↑i) ∧ ∑ i ∈ t', w' i = ∑ i ∈ t, w i ∧ ∑ i ∈ t', w' i • p i = ∑ i ∈ t, w i • p i ∧ ∑ i ∈ t', w' i * c i ≤ ∑ i ∈ t, w i * c i

Carathéodory's elimination, indexed, affine form, with a cost. A convex combination ∑ i ∈ t, w i • p i can be thinned to a sub-index set on which the p i are affinely independent, keeping the value, the total weight and strict positivity, and without increasing the cost ∑ i ∈ t, w i * c i. The cost is what makes this the engine of the function form: with c i = fᵢ(pᵢ) it says thinning never makes the convex-hull value worse. The sign of an affine dependency may be chosen freely because its coefficients sum to zero.

theorem Tdaf.ConvexAnalysis.card_le_finrank_succ_of_affineIndependent {E : Type u_1} [AddCommGroup E] [Module ℝ E] {ι : Type u_2} [FiniteDimensional ℝ E] {p : ι → E} {t : Finset ι} (h : AffineIndependent ℝ fun (i : ↑↑t) => p ↑i) : t.card ≤ Module.finrank ℝ E + 1

Affine independence over an index set bounds the size of the index set by n + 1.

theorem Tdaf.ConvexAnalysis.exists_coalesced_sum {E : Type u_1} [AddCommGroup E] [Module ℝ E] {ι : Type u_2} {C : ι → Set E} (hC : ∀ (i : ι), Convex ℝ (C i)) {κ : Type u_3} (s : Finset κ) (w : κ → ℝ) (z : κ → E) (σ : κ → ι) (hw : ∀ j ∈ s, 0 < w j) (hz : ∀ j ∈ s, z j ∈ C (σ j)) : ∃ (t : Finset ι) (W : ι → ℝ) (Q : ι → E), (∀ i ∈ t, 0 < W i) ∧ (∀ i ∈ t, Q i ∈ C i) ∧ ∑ i ∈ t, W i = ∑ j ∈ s, w j ∧ ∑ i ∈ t, W i • Q i = ∑ j ∈ s, w j • z j

Coalescing — Rockafellar's step "if two of the points with non-zero coefficients belong to the same Cᵢ, the corresponding term can be coalesced". A positive combination of points each drawn from some member of a family of convex sets is rewritten with one point per index, by replacing the points from a single C i by their center of mass.

theorem Tdaf.ConvexAnalysis.exists_linearIndepOn_of_mem_coneHull_iUnion {E : Type u_1} [AddCommGroup E] [Module ℝ E] {ι : Type u_2} [FiniteDimensional ℝ E] {C : ι → Set E} (hC : ∀ (i : ι), Convex ℝ (C i)) {x : E} (hx : x ∈ PointedCone.hull ℝ (⋃ (i : ι), C i)) : ∃ (t : Finset ι) (w : ι → ℝ) (v : ι → E), (∀ i ∈ t, 0 < w i) ∧ (∀ i ∈ t, v i ∈ C i) ∧ LinearIndepOn ℝ v ↑t ∧ t.card ≤ Module.finrank ℝ E ∧ ∑ i ∈ t, w i • v i = x

Every vector of the convex cone generated by a union of convex sets Cᵢ is a non-negative combination of at most n linearly independent vectors, each drawn from a different Cᵢ. The usual statement restricts to non-zero vectors and non-empty Cᵢ; neither is needed, since t = ∅ covers the origin and an empty Cᵢ never contributes an index.

theorem Tdaf.ConvexAnalysis.exists_affineIndependent_of_mem_convexHull_iUnion {E : Type u_1} [AddCommGroup E] [Module ℝ E] {ι : Type u_2} [FiniteDimensional ℝ E] {C : ι → Set E} (hC : ∀ (i : ι), Convex ℝ (C i)) {x : E} (hx : x ∈ (convexHull ℝ) (⋃ (i : ι), C i)) : ∃ (t : Finset ι) (w : ι → ℝ) (p : ι → E), (∀ i ∈ t, 0 < w i) ∧ ∑ i ∈ t, w i = 1 ∧ (∀ i ∈ t, p i ∈ C i) ∧ (AffineIndependent ℝ fun (i : ↑↑t) => p ↑i) ∧ t.card ≤ Module.finrank ℝ E + 1 ∧ ∑ i ∈ t, w i • p i = x

Every point of the convex hull of a union of convex sets Cᵢ is a convex combination of at most n + 1 affinely independent points, each drawn from a different Cᵢ.

Carathéodory for the convex hull of a family of functions

theorem Tdaf.ConvexAnalysis.exists_affineIndependent_of_convFn_lt {E : Type u_1} [AddCommGroup E] [Module ℝ E] [FiniteDimensional ℝ E] {ι : Type u_2} {f : ι → E → EReal} (hf : ∀ (i : ι), ConvexFn (f i)) (hf' : ∀ (i : ι) (x : E), f i x ≠ ⊥) {x : E} {r : ℝ} (h : convFn f x < ↑r) : ∃ (t : Finset ι) (w : ι → ℝ) (p : ι → E), (∀ i ∈ t, 0 < w i) ∧ ∑ i ∈ t, w i = 1 ∧ t.card ≤ Module.finrank ℝ E + 1 ∧ (AffineIndependent ℝ fun (i : ↑↑t) => p ↑i) ∧ (∀ i ∈ t, f i (p i) ≠ ⊤) ∧ ∑ i ∈ t, w i • p i = x ∧ ∑ i ∈ t, ↑(w i) * f i (p i) < ↑r

Any value strictly above (conv {fᵢ})(x) is already achieved by a convex combination in which at most n + 1 coefficients are non-zero, one point per index, and the points carrying a non-zero coefficient are affinely independent. The infimum defining convFn already produces one point per index; the thinning to an affinely independent family is exists_subset_affineIndependent_of_sum with cost c i = fᵢ(pᵢ). The classical proof passes to a "minimal α'" on the vertical line through x, a step that would not be available when conv {fᵢ} is improper and is not needed here.

theorem Tdaf.ConvexAnalysis.convFn_apply_affineIndependent {E : Type u_1} [AddCommGroup E] [Module ℝ E] [FiniteDimensional ℝ E] {ι : Type u_2} {f : ι → E → EReal} (hf : ∀ (i : ι), ConvexFn (f i)) (hf' : ∀ (i : ι) (x : E), f i x ≠ ⊥) (x : E) : convFn f x = sInf {z : EReal | ∃ (t : Finset ι) (w : ι → ℝ) (p : ι → E), (∀ i ∈ t, 0 < w i) ∧ ∑ i ∈ t, w i = 1 ∧ t.card ≤ Module.finrank ℝ E + 1 ∧ (AffineIndependent ℝ fun (i : ↑↑t) => p ↑i) ∧ (∀ i ∈ t, f i (p i) ≠ ⊤) ∧ ∑ i ∈ t, w i • p i = x ∧ z = ∑ i ∈ t, ↑(w i) * f i (p i)}

The convex hull of a family of convex functions is computed by the defining infimum restricted to convex combinations in which at most n + 1 coefficients are non-zero and the corresponding points are affinely independent.

Carathéodory for the convex hull of a single function

theorem Tdaf.ConvexAnalysis.convHullFn_apply_fin {E : Type u_1} [AddCommGroup E] [Module ℝ E] [FiniteDimensional ℝ E] {g : E → EReal} (hg : ∀ (x : E), g x ≠ ⊥) (x : E) : convHullFn g x = sInf {z : EReal | ∃ (w : Fin (Module.finrank ℝ E + 1) → ℝ) (p : Fin (Module.finrank ℝ E + 1) → E), (∀ (i : Fin (Module.finrank ℝ E + 1)), 0 ≤ w i) ∧ ∑ i : Fin (Module.finrank ℝ E + 1), w i = 1 ∧ ∑ i : Fin (Module.finrank ℝ E + 1), w i • p i = x ∧ z = ∑ i : Fin (Module.finrank ℝ E + 1), ↑(w i) * g (p i)}

For an arbitrary function g never taking the value -∞, the convex hull conv g is computed by convex combinations of exactly n + 1 points: (conv g)(x) = inf {∑_{i<n+1} λᵢ g(xᵢ) | ∑ λᵢ xᵢ = x, ∑ λᵢ = 1, λᵢ ≥ 0}. No convexity is assumed, and the points need not be distinct — repetitions and zero coefficients turn "at most n + 1 points" into a statement about the fixed index Fin (n + 1), the convention 0 · (+∞) = 0 making a zero coefficient harmless. Carathéodory applied to epi g would give n + 2 points; the reduction to n + 1 is the elimination run on the base points with the vertical coordinate as its cost.

Which half-spaces contain an intersection of half-spaces

inequalitySet B S is the solution set of the system ⟪x, y⟫ ≤ μ, one inequality per (y, μ) ∈ S. A closed half-space {x | ⟪x, y₀⟫ ≤ μ₀} contains it as soon as (y₀, μ₀) lies in the convex cone generated by S together with (0, 1); the converse holds when that cone is closed, which happens as soon as S is compact and misses the origin.

def Tdaf.ConvexAnalysis.inequalitySet {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (S : Set (F × ℝ)) : Set E

The solution set of the system of linear inequalities ⟪x, y⟫ ≤ μ indexed by (y, μ) ∈ S: an arbitrary intersection of closed half-spaces of E.

Equations

• Tdaf.ConvexAnalysis.inequalitySet B S = {x : E | ∀ q ∈ S, (B x) q.1 ≤ q.2}

theorem Tdaf.ConvexAnalysis.mem_inequalitySet {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {S : Set (F × ℝ)} {x : E} : x ∈ inequalitySet B S ↔ ∀ q ∈ S, (B x) q.1 ≤ q.2

theorem Tdaf.ConvexAnalysis.inequalitySet_subset_halfSpace_of_mem_coneHull {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {S : Set (F × ℝ)} {y₀ : F} {μ₀ : ℝ} (h : (y₀, μ₀) ∈ PointedCone.hull ℝ (insert (0, 1) S)) : inequalitySet B S ⊆ {x : E | (B x) y₀ ≤ μ₀}

A non-negative combination of the given inequalities, with the right-hand side weakened at will, is again valid on the solution set. This half of the representation theorem asks nothing of S.

theorem Tdaf.ConvexAnalysis.mem_coneHull_insert_of_subset_halfSpace {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {S : Set (F × ℝ)} [IsCompatiblePairing B.flip] (hScl : IsClosed S) (hSb : Bornology.IsBounded S) (hS0 : 0 ∉ S) (hint : (interior (inequalitySet B S)).Nonempty) {y₀ : F} {μ₀ : ℝ} (hsub : inequalitySet B S ⊆ {x : E | (B x) y₀ ≤ μ₀}) : (y₀, μ₀) ∈ PointedCone.hull ℝ (insert (0, 1) S)

The converse of inequalitySet_subset_halfSpace_of_mem_coneHull: a closed half-space containing the solution set has its defining pair in the cone generated by S and (0, 1). The pair is separated from that (closed) cone by a functional (y, μ) ↦ ⟪u, y⟫ + c μ with c ≤ 0; a negative c rescales u into a point of the solution set violating the half-space, a vanishing c makes u a direction along which the solution set escapes it.

theorem Tdaf.ConvexAnalysis.exists_card_le_finrank_of_mem_coneHull_insert {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {S : Set (F × ℝ)} (hne : (inequalitySet B S).Nonempty) {y₀ : F} {μ₀ : ℝ} (h : (y₀, μ₀) ∈ PointedCone.hull ℝ (insert (0, 1) S)) : ∃ (t : Finset (F × ℝ)) (l : F × ℝ → ℝ), ↑t ⊆ S ∧ (∀ q ∈ t, 0 ≤ l q) ∧ t.card ≤ Module.finrank ℝ F ∧ ∑ q ∈ t, l q • q.1 = y₀ ∧ ∑ q ∈ t, l q * q.2 ≤ μ₀

Carathéodory's theorem thins a conical representation down to dim F generators drawn from S itself. The upward direction always disappears: either it does not occur, or it can be eliminated, because a maximal linearly independent family of members of S already spans it — and a family of members of S combining to (0, 1) with non-positive coefficients would contradict the existence of a solution.

theorem Tdaf.ConvexAnalysis.mem_coneHull_insert_of_exists_finset {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {S : Set (F × ℝ)} {y₀ : F} {μ₀ : ℝ} {t : Finset (F × ℝ)} {l : F × ℝ → ℝ} (hts : ↑t ⊆ S) (hl : ∀ q ∈ t, 0 ≤ l q) (hfst : ∑ q ∈ t, l q • q.1 = y₀) (hsnd : ∑ q ∈ t, l q * q.2 ≤ μ₀) : (y₀, μ₀) ∈ PointedCone.hull ℝ (insert (0, 1) S)

The elementary direction, packaged for the representation theorem: a non-negative combination of members of S, with the right-hand side weakened, lies in the cone.

theorem Tdaf.ConvexAnalysis.inequalitySet_subset_halfSpace_iff {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {S : Set (F × ℝ)} [IsCompatiblePairing B.flip] (hScl : IsClosed S) (hSb : Bornology.IsBounded S) (hS0 : 0 ∉ S) (hint : (interior (inequalitySet B S)).Nonempty) (y₀ : F) (μ₀ : ℝ) : inequalitySet B S ⊆ {x : E | (B x) y₀ ≤ μ₀} ↔ ∃ (t : Finset (F × ℝ)) (l : F × ℝ → ℝ), ↑t ⊆ S ∧ (∀ q ∈ t, 0 ≤ l q) ∧ t.card ≤ Module.finrank ℝ F ∧ ∑ q ∈ t, l q • q.1 = y₀ ∧ ∑ q ∈ t, l q * q.2 ≤ μ₀

Which closed half-spaces contain the solution set of a compact system of linear inequalities. Let S be a non-empty compact set of pairs (y, μ) missing the origin of F × ℝ, and let C be the solution set of the system ⟪x, y⟫ ≤ μ, (y, μ) ∈ S. If C has interior, then a closed half-space {x | ⟪x, y₀⟫ ≤ μ₀} contains C iff it is a non-negative combination of at most dim F of the given inequalities, with the right-hand side weakened at will.

The hypothesis 0 ∉ S is absent from the classical statement, and is not removable: the proof needs 0 ∉ conv (S ∪ {(0, 1)}), which fails the moment (0, 0) ∈ S, and so does the statement. On F = ℝ² take S = {t (cos φ t, sin φ t, t) | 0 < t ≤ 1} ∪ {0} for a continuous, strictly monotone φ with φ t → φ₀ as t → 0. Then S is compact and C is a neighbourhood of the origin, yet the cone generated by S and (0, 1) meets the plane μ = 1 in a set omitting the unit vector at angle φ₀, and the half-space that vector defines contains C with no representation.