Rockafellar, §17: Carathéodory's Theorem

Carathéodory's theorem for a set S that mixes points and directions, its closedness consequences, and the dual question of which half-spaces contain the solution set of a compact system of linear inequalities.

All ten numbered results of §17 are formalized over Rn n = ℝⁿ: Theorems 17.1–17.3 and Corollaries 17.1.1–17.1.6, 17.2.1.

A mixed set S = S₀ ∪ S₁ is carried as a pair, not as a subset of ℝⁿ: a set P of points and a set D of representative vectors for the directions, one or more per direction. Every construction here is invariant under rescaling a member of D by a positive scalar, so no quotient type is needed. ray D and coneOf D are the book's ray S₁ and cone S₁, and convexHullPD P D is conv S.

Three statements diverge from the book. Corollaries 17.1.4 and 17.1.6 are false as printed: each is recorded as a proposition (corollary_17_1_4, corollary_17_1_6) and refuted on ℝ¹ (corollary_17_1_4_false, corollary_17_1_6_false). Theorem 17.3 is false without 0 ∉ S*, so theorem_17_3 carries that hypothesis; the book's x* ≠ 0 is conversely unnecessary.

References

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

Points and directions

def Rockafellar.ray {n : ℕ} (D : Set (TdafSurface.Rn n)) : Set (TdafSurface.Rn n)

ray S₁ (p. 153): the origin together with all vectors whose directions belong to S₁, represented here by a set D of vectors, one or more per direction.

Equations

• Rockafellar.ray D = insert 0 {x : TdafSurface.Rn n | ∃ y ∈ D, ∃ (a : ℝ), 0 < a ∧ x = a • y}

def Rockafellar.coneOf {n : ℕ} (D : Set (TdafSurface.Rn n)) : Set (TdafSurface.Rn n)

cone S₁ (p. 153): the convex cone generated by the vectors of D. The book defines it as conv (ray S₁); coneOf_eq_convexHull_ray is the bridge.

Equations

• Rockafellar.coneOf D = ↑(PointedCone.hull ℝ D)

theorem Rockafellar.subset_ray {n : ℕ} (D : Set (TdafSurface.Rn n)) : D ⊆ ray D

theorem Rockafellar.ray_subset_coneOf {n : ℕ} (D : Set (TdafSurface.Rn n)) : ray D ⊆ coneOf D

theorem Rockafellar.coneOf_eq_convexHull_ray {n : ℕ} (D : Set (TdafSurface.Rn n)) : coneOf D = (convexHull ℝ) (ray D)

Rockafellar's definition cone S₁ = conv (ray S₁), for any set of representative vectors.

theorem Rockafellar.convexHullPD_eq_add {n : ℕ} (P D : Set (TdafSurface.Rn n)) : Tdaf.ConvexAnalysis.convexHullPD P D = (convexHull ℝ) P + coneOf D

conv S = conv S₀ + cone S₁ (p. 153): the book's formula for the convex hull of a mixed set, which is the backbone's definition of convexHullPD.

theorem Rockafellar.convexHullPD_isLeast {n : ℕ} (P D : Set (TdafSurface.Rn n)) : IsLeast {C : Set (TdafSurface.Rn n) | Convex ℝ C ∧ P ⊆ C ∧ D ⊆ Tdaf.ConvexAnalysis.recessionCone C} (Tdaf.ConvexAnalysis.convexHullPD P D)

Rockafellar's definition of conv S (p. 153): the smallest convex set containing S₀ and receding in every direction of S₁.

theorem Rockafellar.convexHullPD_empty_points {n : ℕ} (D : Set (TdafSurface.Rn n)) : Tdaf.ConvexAnalysis.convexHullPD ∅ D = ∅

aff S = conv S = ∅ if S contains directions only (p. 154).

Theorem 17.1

theorem Rockafellar.theorem_17_1 {n : ℕ} (P D : Set (TdafSurface.Rn n)) (x : TdafSurface.Rn n) : x ∈ Tdaf.ConvexAnalysis.convexHullPD P D ↔ ∃ (p : Finset (TdafSurface.Rn n)) (d : Finset (TdafSurface.Rn n)) (a : TdafSurface.Rn n → ℝ) (b : TdafSurface.Rn n → ℝ), ↑p ⊆ P ∧ ↑d ⊆ D ∧ (∀ y ∈ p, 0 < a y) ∧ (∀ y ∈ d, 0 < b y) ∧ ∑ y ∈ p, a y = 1 ∧ p.card + d.card ≤ n + 1 ∧ ∑ y ∈ p, a y • y + ∑ y ∈ d, b y • y = x

Theorem 17.1 (Carathéodory's Theorem). For a set S of points and directions in ℝⁿ, x ∈ conv S iff x is a convex combination of n + 1 of the points and directions of S, not necessarily distinct. The count is the total number of points and directions used, and every coefficient produced is strictly positive.

theorem Rockafellar.theorem_17_1_simplex {n : ℕ} {P D : Set (TdafSurface.Rn n)} (hP : P.Nonempty) {m : ℕ} (hm : dim (Tdaf.ConvexAnalysis.convexHullPD P D) = ↑m) : Tdaf.ConvexAnalysis.convexHullPD P D = ⋃ (p : Finset (TdafSurface.Rn n)), ⋃ (d : Finset (TdafSurface.Rn n)), ⋃ (_ : ↑p ⊆ P), ⋃ (_ : ↑d ⊆ D), ⋃ (_ : Tdaf.ConvexAnalysis.AffineIndepPD ↑p ↑d), ⋃ (_ : p.card + d.card = m + 1), Tdaf.ConvexAnalysis.convexHullPD ↑p ↑d

Theorem 17.1, second sentence: conv S is the union of the generalized d-dimensional simplices whose vertices belong to S, where d = dim (conv S). A generalized d-dimensional simplex (p. 155) is convexHullPD of d + 1 affinely independent points and directions — the points its ordinary vertices, the directions its vertices at infinity — affine independence of a mixed set meaning that the lifted vectors (1, xᵢ) and (0, xⱼ) are linearly independent in ℝⁿ⁺¹. The hypothesis P ≠ ∅ is the book's convention conv S = ∅ for directions only.

theorem Rockafellar.corollary_17_1_1 {n : ℕ} {ι : Type u_1} {C : ι → Set (TdafSurface.Rn n)} (hC : ∀ (i : ι), Convex ℝ (C i)) {x : TdafSurface.Rn n} (hx : x ∈ (convexHull ℝ) (⋃ (i : ι), C i)) : ∃ (t : Finset ι) (w : ι → ℝ) (p : ι → TdafSurface.Rn n), (∀ i ∈ t, 0 < w i) ∧ ∑ i ∈ t, w i = 1 ∧ (∀ i ∈ t, p i ∈ C i) ∧ (AffineIndependent ℝ fun (i : ↑↑t) => p ↑i) ∧ t.card ≤ n + 1 ∧ ∑ i ∈ t, w i • p i = x

Corollary 17.1.1. Every point of the convex hull of a union of convex sets Cᵢ is a convex combination of n + 1 or fewer affinely independent points, each from a different Cᵢ.

theorem Rockafellar.corollary_17_1_2 {n : ℕ} {ι : Type u_1} {C : ι → Set (TdafSurface.Rn n)} (hC : ∀ (i : ι), Convex ℝ (C i)) {x : TdafSurface.Rn n} (hx : x ∈ coneOf (⋃ (i : ι), C i)) : ∃ (t : Finset ι) (w : ι → ℝ) (v : ι → TdafSurface.Rn n), (∀ i ∈ t, 0 < w i) ∧ (∀ i ∈ t, v i ∈ C i) ∧ LinearIndepOn ℝ v ↑t ∧ t.card ≤ n ∧ ∑ i ∈ t, w i • v i = x

Corollary 17.1.2. Every vector of the convex cone generated by a union of convex sets Cᵢ is a non-negative combination of n or fewer linearly independent vectors, each from a different Cᵢ. Neither the book's x ≠ 0 nor its Cᵢ ≠ ∅ is needed: the empty index set covers the origin, and an empty Cᵢ never contributes an index.

theorem Rockafellar.corollary_17_1_3 {n : ℕ} {ι : Type u_1} {f : ι → TdafSurface.Rn n → EReal} (hf : ∀ (i : ι), Tdaf.ConvexAnalysis.ConvexFn (f i)) (hp : ∀ (i : ι), Tdaf.ConvexAnalysis.Proper (f i)) (x : TdafSurface.Rn n) : Tdaf.ConvexAnalysis.convFn f x = sInf {z : EReal | ∃ (t : Finset ι) (w : ι → ℝ) (p : ι → TdafSurface.Rn n), (∀ i ∈ t, 0 < w i) ∧ ∑ i ∈ t, w i = 1 ∧ t.card ≤ n + 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)}

Corollary 17.1.3. For proper convex fᵢ, (conv fᵢ) x is the infimum of ∑ λᵢ fᵢ(xᵢ) over convex combinations ∑ λᵢ xᵢ = x with at most n + 1 non-zero coefficients whose xᵢ are affinely independent. The elimination behind it may choose the sign of an affine dependency by the cost, both signs carrying a positive coefficient; that is what fails for Corollary 17.1.4.

theorem Rockafellar.corollary_17_1_5 {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : ∀ (x : TdafSurface.Rn n), f x ≠ ⊥) (x : TdafSurface.Rn n) : Tdaf.ConvexAnalysis.convHullFn f x = sInf {z : EReal | ∃ (w : Fin (n + 1) → ℝ) (p : Fin (n + 1) → TdafSurface.Rn n), (∀ (i : Fin (n + 1)), 0 ≤ w i) ∧ ∑ i : Fin (n + 1), w i = 1 ∧ ∑ i : Fin (n + 1), w i • p i = x ∧ z = ∑ i : Fin (n + 1), ↑(w i) * f (p i)}

Corollary 17.1.5. For any f : ℝⁿ → (-∞, +∞], (conv f) x is the infimum of ∑_{i=1}^{n+1} λᵢ f(xᵢ) over convex combinations ∑ λᵢ xᵢ = x. The points need not be distinct: repetitions and zero coefficients turn Carathéodory's "at most n + 1" into a statement about the fixed index type Fin (n + 1), and 0 · (+∞) = 0 makes a zero coefficient harmless.

Theorems 17.2 and 17.3

theorem Rockafellar.theorem_17_2 {n : ℕ} {S : Set (TdafSurface.Rn n)} (hS : Bornology.IsBounded S) : closure ((convexHull ℝ) S) = (convexHull ℝ) (closure S)

Theorem 17.2. cl (conv S) = conv (cl S) for a bounded set S ⊆ ℝⁿ.

theorem Rockafellar.theorem_17_2_isCompact {n : ℕ} {S : Set (TdafSurface.Rn n)} (hS : IsCompact S) : IsCompact ((convexHull ℝ) S)

Theorem 17.2, second sentence: conv S is closed and bounded whenever S is. In ℝⁿ "closed and bounded" is "compact".

theorem Rockafellar.corollary_17_2_1 {n : ℕ} {S : Set (TdafSurface.Rn n)} (hSne : S.Nonempty) (hScl : IsClosed S) (hSb : Bornology.IsBounded S) {h : TdafSurface.Rn n → ℝ} (hcont : ContinuousOn h S) : Tdaf.ConvexAnalysis.ClosedProperConvexFn (Tdaf.ConvexAnalysis.convHullFn (Tdaf.ConvexAnalysis.restrict S fun (x : TdafSurface.Rn n) => ↑(h x)))

Corollary 17.2.1. If S is non-empty, closed and bounded and h is continuous on S, the convex hull of h extended by +∞ off S is a closed proper convex function.

theorem Rockafellar.theorem_17_3 {n : ℕ} {S : Set (TdafSurface.Rn n × ℝ)} (hScl : IsClosed S) (hSb : Bornology.IsBounded S) (hS0 : 0 ∉ S) (hdim : dim (Tdaf.ConvexAnalysis.inequalitySet (TdafSurface.pairing n) S) = ↑n) (b : TdafSurface.Rn n) (β : ℝ) : Tdaf.ConvexAnalysis.inequalitySet (TdafSurface.pairing n) S ⊆ {x : TdafSurface.Rn n | ((TdafSurface.pairing n) x) b ≤ β} ↔ ∃ (t : Finset (TdafSurface.Rn n × ℝ)) (l : TdafSurface.Rn n × ℝ → ℝ), ↑t ⊆ S ∧ (∀ q ∈ t, 0 ≤ l q) ∧ t.card ≤ n ∧ ∑ q ∈ t, l q • q.1 = b ∧ ∑ q ∈ t, l q * q.2 ≤ β

Theorem 17.3. Let S* be a non-empty closed bounded set of vectors (x*, μ*) in ℝⁿ⁺¹ and let C = {x | ⟨x, x*⟩ ≤ μ* for all (x*, μ*) ∈ S*} be n-dimensional. The half-space {x | ⟨x, b⟩ ≤ β} contains C iff b = ∑ λᵢ xᵢ* and ∑ λᵢ μᵢ* ≤ β for some (xᵢ*, μᵢ*) ∈ S* and λᵢ ≥ 0, at most n terms in all.

The book's statement is false without 0 ∉ S*, which is assumed here: its proof concludes that the origin of ℝⁿ⁺¹ lies outside conv (S* ∪ {(0,1)}), and that fails as soon as (0,0) ∈ S*. The book's x* ≠ 0 is conversely unnecessary — the empty combination covers it.

Corollaries 17.1.4 and 17.1.6: stated and refuted

def Rockafellar.corollary_17_1_4 : Prop

Corollary 17.1.4 as the book states it: for proper convex fᵢ and f the positively homogeneous convex function generated by conv {fᵢ}, f x for x ≠ 0 is the infimum of ∑ λᵢ fᵢ(xᵢ) over non-negative combinations ∑ λᵢ xᵢ = x with at most n non-zero coefficients whose xᵢ are linearly independent. The proposition is false, and corollary_17_1_4_false refutes it; it is stated because the book prints it as a corollary with a proof.

Equations

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

theorem Rockafellar.corollary_17_1_4_false : ¬corollary_17_1_4

Corollary 17.1.4 is false as stated. On ℝ¹ take f₁ y = -y and f₂ y = y, both proper convex. Then conv {f₁, f₂} ≡ -∞, since the midpoint of (y + s, f₁(y + s)) and (y - s, f₂(y - s)) is (y, -s) for every s > 0, so the positively homogeneous convex function generated is -∞ everywhere; but at x = e ≠ 0 the infimum on the right is -1, because n = 1 admits a single index and λ x₁ = e forces the value -1 or 1.

The elimination that proves Corollary 17.1.3 has no conical analogue: an affine dependency has coefficients summing to zero, so both signs occur and one may be chosen to lower the cost, whereas a conical dependency can have every coefficient of one sign.

def Rockafellar.corollary_17_1_6 : Prop

Corollary 17.1.6 as the book states it: for f : ℝⁿ → (-∞, +∞] and k the positively homogeneous convex function generated by conv f, k x for x ≠ 0 is the infimum of ∑_{i=1}^{n} λᵢ f(xᵢ) over non-negative combinations ∑ λᵢ xᵢ = x. The proposition is false, and corollary_17_1_6_false refutes it.

Equations

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

theorem Rockafellar.corollary_17_1_6_false : ¬corollary_17_1_6

Corollary 17.1.6 is false as stated. On ℝ¹ take f y = -|y|, which never takes the value -∞. Then conv f ≡ -∞, because the midpoint of (y + s, -|y + s|) and (y - s, -|y - s|) is (y, α) with α ≤ -s for every s > 0, so the generated k is -∞ everywhere. At x = e ≠ 0, however, n = 1 admits one vector and λ x₁ = e with λ ≥ 0 forces λ f(x₁) = -1, so the infimum is -1. This is Corollary 17.1.4's failure for a one-element family.