Rockafellar, §2: Convex Sets and Cones

Convex sets, convex hulls and convex combinations; the dimension of a convex set; cones, convex cones and the smallest convex cone including a set. All 13 numbered results of §2 are formalized. The section is thin: eight of them are one-line specialisations of Mathlib's Convex/convexHull API, and Theorem 2.6 is the backbone's convex_iff_add_mem_of_isCone verbatim.

Main definitions

• IsCone — the book's cone: closed under positive scalar multiplication, with the origin free to belong or not. Deliberately not Mathlib's PointedCone, which contains 0 by definition; the cones produced by Corollaries 2.6.2 and 2.6.3 need not contain the origin. isCone_iff_smul_set_eq bridges to the backbone's ∀ a > 0, a • s = s, and toPointedCone bridges to Mathlib when 0 ∈ K, which is the hypothesis of Theorem 2.7.
• posCombinations — the positive linear combinations of a set, the object of Corollaries 2.6.1 and 2.6.2.

The dimension of a convex set is dim from §1: the dimension of the subspace parallel to aff C.

Theorem 2.7 is split into four declarations, because the book's single sentence asserts four things.

References

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

Rockafellar's cones

def Rockafellar.IsCone {n : ℕ} (K : Set (TdafSurface.Rn n)) : Prop

Rockafellar's cone: a subset of ℝⁿ closed under positive scalar multiplication, the origin free to belong or not. Not Mathlib's PointedCone, which contains 0 by definition; Corollaries 2.6.2 and 2.6.3 produce cones that need not contain the origin.

Equations

• Rockafellar.IsCone K = ∀ (l : ℝ), 0 < l → ∀ x ∈ K, l • x ∈ K

theorem Rockafellar.isCone_iff_smul_set_eq {n : ℕ} (K : Set (TdafSurface.Rn n)) : IsCone K ↔ ∀ (a : ℝ), 0 < a → a • K = K

IsCone in the backbone's spelling ∀ a > 0, a • s = s, which is the hypothesis of smul_mem_iff_of_isCone and convex_iff_add_mem_of_isCone.

Intersections: Theorems 2.1 and 2.5

theorem Rockafellar.theorem_2_1 {n : ℕ} (𝒞 : Set (Set (TdafSurface.Rn n))) (h : ∀ C ∈ 𝒞, Convex ℝ C) : Convex ℝ (⋂₀ 𝒞)

Theorem 2.1. The intersection of an arbitrary collection of convex sets is convex.

theorem Rockafellar.corollary_2_1_1 {n : ℕ} {ι : Type u_1} (b : ι → TdafSurface.Rn n) (β : ι → ℝ) : Convex ℝ {x : TdafSurface.Rn n | ∀ (i : ι), ((TdafSurface.pairing n) x) (b i) ≤ β i}

Corollary 2.1.1. The solution set {x | ⟨x, bᵢ⟩ ≤ βᵢ for all i} of an arbitrary system of weak linear inequalities is convex.

theorem Rockafellar.theorem_2_5 {n : ℕ} (𝒦 : Set (Set (TdafSurface.Rn n))) (h : ∀ K ∈ 𝒦, IsCone K ∧ Convex ℝ K) : IsCone (⋂₀ 𝒦) ∧ Convex ℝ (⋂₀ 𝒦)

Theorem 2.5. The intersection of an arbitrary collection of convex cones is a convex cone.

theorem Rockafellar.corollary_2_5_1 {n : ℕ} {ι : Type u_1} (b : ι → TdafSurface.Rn n) : IsCone {x : TdafSurface.Rn n | ∀ (i : ι), ((TdafSurface.pairing n) x) (b i) ≤ 0} ∧ Convex ℝ {x : TdafSurface.Rn n | ∀ (i : ι), ((TdafSurface.pairing n) x) (b i) ≤ 0}

Corollary 2.5.1. The solution set of a homogeneous system of weak linear inequalities is a convex cone.

Convex combinations: Theorems 2.2, 2.3 and 2.4

theorem Rockafellar.theorem_2_2 {n : ℕ} (C : Set (TdafSurface.Rn n)) : Convex ℝ C ↔ ∀ (k : ℕ) (l : Fin k → ℝ) (x : Fin k → TdafSurface.Rn n), (∀ (i : Fin k), 0 ≤ l i) → ∑ i : Fin k, l i = 1 → (∀ (i : Fin k), x i ∈ C) → ∑ i : Fin k, l i • x i ∈ C

Theorem 2.2. A subset of ℝⁿ is convex iff it contains all convex combinations of its elements.

theorem Rockafellar.theorem_2_3 {n : ℕ} (S : Set (TdafSurface.Rn n)) : (convexHull ℝ) S = {z : TdafSurface.Rn n | ∃ (k : ℕ) (l : Fin k → ℝ) (x : Fin k → TdafSurface.Rn n), (∀ (i : Fin k), 0 ≤ l i) ∧ ∑ i : Fin k, l i = 1 ∧ (∀ (i : Fin k), x i ∈ S) ∧ ∑ i : Fin k, l i • x i = z}

Theorem 2.3. For any S ⊆ ℝⁿ, conv S consists of all convex combinations of elements of S. Indexed by Fin k, so that the statement reads as the book's λ₁x₁ + ⋯ + λ_m x_m.

theorem Rockafellar.corollary_2_3_1 {n k : ℕ} (b : Fin (k + 1) → TdafSurface.Rn n) : (convexHull ℝ) (Set.range b) = {z : TdafSurface.Rn n | ∃ (l : Fin (k + 1) → ℝ), (∀ (i : Fin (k + 1)), 0 ≤ l i) ∧ ∑ i : Fin (k + 1), l i = 1 ∧ ∑ i : Fin (k + 1), l i • b i = z}

Corollary 2.3.1. The convex hull of {b₀, …, b_m} is the set of λ₀b₀ + ⋯ + λ_m b_m with λᵢ ≥ 0 and λ₀ + ⋯ + λ_m = 1.

theorem Rockafellar.theorem_2_4 {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hne : C.Nonempty) : IsGreatest {d : ℤ | ∃ (b : Set (TdafSurface.Rn n)), AffineIndependent ℝ Subtype.val ∧ (convexHull ℝ) b ⊆ C ∧ d = dim ((convexHull ℝ) b)} (dim C)

Theorem 2.4. The dimension of a convex set C is the largest dimension of a simplex included in C. A simplex is the convex hull of an affinely independent set, which in ℝⁿ is automatically finite, so no finiteness hypothesis is carried. Needs C non-empty, which the book does not say: for C = ∅ there is no simplex at all, and the maximum does not exist.

Convex cones: Theorems 2.6 and 2.7

theorem Rockafellar.theorem_2_6 {n : ℕ} (K : Set (TdafSurface.Rn n)) : IsCone K ∧ Convex ℝ K ↔ (∀ x ∈ K, ∀ y ∈ K, x + y ∈ K) ∧ ∀ (l : ℝ), 0 < l → ∀ x ∈ K, l • x ∈ K

Theorem 2.6. A subset of ℝⁿ is a convex cone iff it is closed under addition and positive scalar multiplication.

def Rockafellar.posCombinations {n : ℕ} (S : Set (TdafSurface.Rn n)) : Set (TdafSurface.Rn n)

Rockafellar's positive linear combinations of S: the sums λ₁x₁ + ⋯ + λ_m x_m with m ≥ 1, every λᵢ > 0 and every xᵢ ∈ S. The index is an arbitrary non-empty finite type rather than Fin (m+1), which makes the concatenation in Corollary 2.6.2 a Sum.

Equations

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

theorem Rockafellar.posCombinations_mono {n : ℕ} {S T : Set (TdafSurface.Rn n)} (h : S ⊆ T) : posCombinations S ⊆ posCombinations T

Positive linear combinations are monotone in the set.

theorem Rockafellar.subset_posCombinations {n : ℕ} (S : Set (TdafSurface.Rn n)) : S ⊆ posCombinations S

A one-term positive combination is the element itself.

theorem Rockafellar.corollary_2_6_1 {n : ℕ} (K : Set (TdafSurface.Rn n)) : IsCone K ∧ Convex ℝ K ↔ posCombinations K ⊆ K

Corollary 2.6.1. A subset of ℝⁿ is a convex cone iff it contains all positive linear combinations of its elements.

theorem Rockafellar.corollary_2_6_2 {n : ℕ} (S : Set (TdafSurface.Rn n)) : IsLeast {K : Set (TdafSurface.Rn n) | IsCone K ∧ Convex ℝ K ∧ S ⊆ K} (posCombinations S)

Corollary 2.6.2. The positive linear combinations of S form the smallest convex cone including S. This cone need not contain the origin: it is the book's cone S only after the origin is adjoined.

theorem Rockafellar.corollary_2_6_3 {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) : IsLeast {K : Set (TdafSurface.Rn n) | IsCone K ∧ Convex ℝ K ∧ C ⊆ K} {z : TdafSurface.Rn n | ∃ (l : ℝ), 0 < l ∧ ∃ x ∈ C, l • x = z}

Corollary 2.6.3. For a convex set C, the set {λx | λ > 0, x ∈ C} is the smallest convex cone which includes C.

def Rockafellar.toPointedCone {n : ℕ} {K : Set (TdafSurface.Rn n)} (hK : IsCone K) (hconv : Convex ℝ K) (h0 : 0 ∈ K) : PointedCone ℝ (TdafSurface.Rn n)

A convex cone containing the origin, bundled as a Mathlib PointedCone. This is the bridge Theorem 2.7 crosses: Rockafellar's cone plus 0 ∈ K is exactly PointedCone.

Equations

• Rockafellar.toPointedCone hK hconv h0 = { carrier := K, add_mem' := ⋯, zero_mem' := h0, smul_mem' := ⋯ }

@[simp]

theorem Rockafellar.coe_toPointedCone {n : ℕ} {K : Set (TdafSurface.Rn n)} (hK : IsCone K) (hconv : Convex ℝ K) (h0 : 0 ∈ K) : ↑(toPointedCone hK hconv h0) = K

The carrier of toPointedCone is the set it came from.

theorem Rockafellar.theorem_2_7_greatest {n : ℕ} {K : Set (TdafSurface.Rn n)} (hK : IsCone K) (hconv : Convex ℝ K) (h0 : 0 ∈ K) : ∃ (L : Submodule ℝ (TdafSurface.Rn n)), ↑L = -K ∩ K ∧ IsGreatest {L' : Submodule ℝ (TdafSurface.Rn n) | ↑L' ⊆ K} L

Theorem 2.7, second half: for a convex cone K containing 0 there is a largest subspace contained in K, namely (-K) ∩ K.

theorem Rockafellar.theorem_2_7_least {n : ℕ} (K : Set (TdafSurface.Rn n)) : IsLeast {L : Submodule ℝ (TdafSurface.Rn n) | K ⊆ ↑L} (Submodule.span ℝ K)

Theorem 2.7, first half: the smallest subspace containing a set is its linear span.

theorem Rockafellar.theorem_2_7_sub {n : ℕ} {K : Set (TdafSurface.Rn n)} (hK : IsCone K) (hconv : Convex ℝ K) (h0 : 0 ∈ K) : ↑(Submodule.span ℝ K) = K - K

Theorem 2.7, first half continued: for a convex cone K containing 0, that smallest subspace is K - K.

theorem Rockafellar.theorem_2_7_aff {n : ℕ} {K : Set (TdafSurface.Rn n)} (h0 : 0 ∈ K) : ↑(Submodule.span ℝ K) = ↑(affineSpan ℝ K)

Theorem 2.7, first half continued: that smallest subspace is aff K. This is the last sentence of the book's proof — the affine hull of a set containing 0 is a subspace, by Theorem 1.1.