Rockafellar, §3: The Algebra of Convex Sets

Operations that preserve convexity: scalar multiples, sums, convex combinations of a family of sets, images and inverse images under linear maps, direct sums, partial addition, and the inverse sum. All 9 numbered results of §3 are formalized.

Main definitions

• convexCombinations — the union of all finite convex combinations ∑ λᵢ Cᵢ of a family of sets, which is the right-hand side of Theorem 3.3.
• partialAdd — the partial addition of Theorem 3.6: add in the second argument, intersect in the first. The book describes the operation informally and fixes no symbol for it, so its commutativity, associativity and two extreme cases (m = 0 is ordinary addition, p = 0 is intersection) are proved here; §5 rests on them.
• invSum — Rockafellar's inverse sum C₁ # C₂. It has no backbone counterpart, so it comes with three bridges: mem_invSum_iff_exists, invSum_eq_iUnion_singleton, and invSum_eq_partialAdd_coneLift, the derivation from partial addition that Theorem 3.7's one-line proof appeals to.
• coneLift — the convex cone in ℝⁿ⁺¹ with cross-section C, through which the book derives # from partial addition.

λC, −C and C₁ + C₂ need no definition of their own: they are Mathlib's pointwise a • s, -s and s + t, and the book's displayed formulas for them are those definitions on the nose. ℝᵐ⁺ᵖ is Rn m × Rn p here, which is the shape in which §3 actually uses it — a vector of ℝᵐ⁺ᵖ is written (y, z) throughout. theorem_3_8_invSum drops the convexity the book assumes, its proof not using it; theorem_3_8_add keeps it.

References

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

Scalar multiples, reflections and sums

theorem Rockafellar.zero_mem_of_neg_eq_self {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hne : C.Nonempty) (hsym : -C = C) : 0 ∈ C

A non-empty symmetric convex set contains the origin: along with each x it contains -x, hence the whole segment between them.

theorem Rockafellar.theorem_3_1 {n : ℕ} {C₁ C₂ : Set (TdafSurface.Rn n)} (h₁ : Convex ℝ C₁) (h₂ : Convex ℝ C₂) : Convex ℝ (C₁ + C₂)

Theorem 3.1. The sum C₁ + C₂ = {x₁ + x₂ | x₁ ∈ C₁, x₂ ∈ C₂} of two convex sets is convex.

theorem Rockafellar.zero_mem_add_neg {n : ℕ} {C : Set (TdafSurface.Rn n)} (hne : C.Nonempty) : 0 ∈ C + -C

Additive inverses do not exist for sets with more than one point; the best one can say in general is that 0 ∈ C + (-C) when C ≠ ∅.

theorem Rockafellar.theorem_3_2 {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) {l₁ l₂ : ℝ} (h₁ : 0 ≤ l₁) (h₂ : 0 ≤ l₂) : (l₁ + l₂) • C = l₁ • C + l₂ • C

Theorem 3.2. (λ₁ + λ₂) C = λ₁ C + λ₂ C for convex C and λ₁, λ₂ ≥ 0. This is the one law of set algebra in §3 that depends on convexity: ⊆ holds for any C, and ⊇ is the convexity relation C ⊇ (λ₁/(λ₁+λ₂)) C + (λ₂/(λ₁+λ₂)) C multiplied through by λ₁ + λ₂.

theorem Rockafellar.smul_add_smul_self {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) {l : ℝ} (h₀ : 0 ≤ l) (h₁ : l ≤ 1) : (1 - l) • C + l • C = C

Rockafellar, §3 (p. 17). Convexity of C says (1 - λ) C + λ C ⊆ C for 0 < λ < 1; Theorem 3.2 is what upgrades that inclusion to an equality.

theorem Rockafellar.add_self_eq_two_smul {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) : C + C = 2 • C

Rockafellar, §3 (p. 19). C + C = 2C for convex C, the first consequence the book draws from Theorem 3.2.

Theorem 3.3: the convex hull of a union

def Rockafellar.convexCombinations {n : ℕ} {I : Type u_1} (C : I → Set (TdafSurface.Rn n)) : Set (TdafSurface.Rn n)

The right-hand side of Theorem 3.3: the union of all finite convex combinations λ₁ C_{i₁} + ⋯ + λ_m C_{i_m} of the family C, taken over all non-negative choices of the coefficients λᵢ of which only finitely many are non-zero and which add up to 1.

Equations

• Rockafellar.convexCombinations C = ⋃ (s : Finset I), ⋃ (w : I → ℝ), ⋃ (_ : ∀ i ∈ s, 0 ≤ w i), ⋃ (_ : ∑ i ∈ s, w i = 1), ∑ i ∈ s, w i • C i

theorem Rockafellar.mem_convexCombinations {n : ℕ} {I : Type u_1} {C : I → Set (TdafSurface.Rn n)} {x : TdafSurface.Rn n} : x ∈ convexCombinations C ↔ ∃ (s : Finset I) (w : I → ℝ), (∀ i ∈ s, 0 ≤ w i) ∧ ∑ i ∈ s, w i = 1 ∧ x ∈ ∑ i ∈ s, w i • C i

Membership in convexCombinations, with the four nested unions unpacked.

theorem Rockafellar.theorem_3_3 {n : ℕ} {I : Type u_1} {C : I → Set (TdafSurface.Rn n)} (hC : ∀ (i : I), Convex ℝ (C i)) (hne : ∀ (i : I), (C i).Nonempty) : (convexHull ℝ) (⋃ (i : I), C i) = convexCombinations C

Theorem 3.3. The convex hull of the union of a collection of non-empty convex sets Cᵢ is ⋃ ∑ᵢ λᵢ Cᵢ, the union over all non-negative coefficient families with finite support summing to 1.

Theorem 3.4: images and inverse images

theorem Rockafellar.theorem_3_4_image {n m : ℕ} (A : TdafSurface.Rn n →ₗ[ℝ] TdafSurface.Rn m) {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) : Convex ℝ (⇑A '' C)

Theorem 3.4 (first clause). The image AC = {Ax | x ∈ C} of a convex set under a linear transformation is convex.

theorem Rockafellar.theorem_3_4_preimage {n m : ℕ} (A : TdafSurface.Rn n →ₗ[ℝ] TdafSurface.Rn m) {D : Set (TdafSurface.Rn m)} (hD : Convex ℝ D) : Convex ℝ (⇑A ⁻¹' D)

Theorem 3.4 (second clause). The inverse image A⁻¹D = {x | Ax ∈ D} of a convex set is convex. The notation does not imply that A is invertible.

theorem Rockafellar.corollary_3_4_1 {n : ℕ} (L : Submodule ℝ (TdafSurface.Rn n)) [L.HasOrthogonalProjection] {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) : Convex ℝ (⇑L.starProjection '' C)

Corollary 3.4.1. The orthogonal projection of a convex set C on a subspace L is another convex set: the projection assigns to each x the unique y ∈ L with x - y ⊥ L, and that assignment is linear, so Theorem 3.4 applies.

Theorem 3.5: the direct sum

theorem Rockafellar.theorem_3_5 {m p : ℕ} {C : Set (TdafSurface.Rn m)} {D : Set (TdafSurface.Rn p)} (hC : Convex ℝ C) (hD : Convex ℝ D) : Convex ℝ (C ×ˢ D)

Theorem 3.5. The direct sum C ⊕ D = {(y, z) | y ∈ C, z ∈ D} of convex sets is convex. C ⊕ D is Mathlib's C ×ˢ D, on Rn m × Rn p rather than Rn (m + p).

theorem Rockafellar.directSum_iff_unique {n : ℕ} {C D : Set (TdafSurface.Rn n)} (hC : C.Nonempty) (hD : D.Nonempty) : (∀ y₁ ∈ C, ∀ z₁ ∈ D, ∀ y₂ ∈ C, ∀ z₂ ∈ D, y₁ + z₁ = y₂ + z₂ → y₁ = y₂ ∧ z₁ = z₂) ↔ (C - C) ∩ (D - D) = {0}

Each x ∈ C + D decomposes uniquely as x = y + z with y ∈ C, z ∈ D — the case in which C + D is also called a direct sum — iff (C - C) ∩ (D - D) = {0}. The book states this without proof.

Theorem 3.6: partial addition

def Rockafellar.partialAdd {Y : Type u_1} {Z : Type u_2} [Add Z] (C₁ C₂ : Set (Y × Z)) : Set (Y × Z)

Partial addition, the operation of Theorem 3.6: partialAdd C₁ C₂ is the set of (y, z) for which there are z₁, z₂ with (y, z₁) ∈ C₁, (y, z₂) ∈ C₂ and z₁ + z₂ = z. The book describes this in words as "adding in the z argument alone" and fixes no symbol for it; there is one such operation for each decomposition of ℝⁿ into a direct sum of two subspaces.

Equations

• Rockafellar.partialAdd C₁ C₂ = {q : Y × Z | ∃ (z₁ : Z) (z₂ : Z), (q.1, z₁) ∈ C₁ ∧ (q.1, z₂) ∈ C₂ ∧ z₁ + z₂ = q.2}

@[simp]

theorem Rockafellar.mem_partialAdd {Y : Type u_1} {Z : Type u_2} [Add Z] {C₁ C₂ : Set (Y × Z)} {y : Y} {z : Z} : (y, z) ∈ partialAdd C₁ C₂ ↔ ∃ (z₁ : Z) (z₂ : Z), (y, z₁) ∈ C₁ ∧ (y, z₂) ∈ C₂ ∧ z₁ + z₂ = z

Membership in partialAdd, at an explicit pair.

theorem Rockafellar.partialAdd_comm {Y : Type u_1} {Z : Type u_2} [AddCommMonoid Z] (C₁ C₂ : Set (Y × Z)) : partialAdd C₁ C₂ = partialAdd C₂ C₁

Rockafellar, §3 (p. 20). Partial addition is commutative.

theorem Rockafellar.partialAdd_assoc {Y : Type u_1} {Z : Type u_2} [AddCommMonoid Z] (C₁ C₂ C₃ : Set (Y × Z)) : partialAdd (partialAdd C₁ C₂) C₃ = partialAdd C₁ (partialAdd C₂ C₃)

Rockafellar, §3 (p. 20). Partial addition is associative.

theorem Rockafellar.partialAdd_eq_add {Y : Type u_1} {Z : Type u_2} [Add Y] [Add Z] [Subsingleton Y] (C₁ C₂ : Set (Y × Z)) : partialAdd C₁ C₂ = C₁ + C₂

Rockafellar, §3 (p. 20), the extreme case m = 0. When the first factor is trivial, partial addition is ordinary addition of sets.

theorem Rockafellar.partialAdd_eq_inter {Y : Type u_1} {Z : Type u_2} [Add Z] [Subsingleton Z] (C₁ C₂ : Set (Y × Z)) : partialAdd C₁ C₂ = C₁ ∩ C₂

Rockafellar, §3 (p. 20), the extreme case p = 0. When the second factor is trivial, partial addition is intersection.

theorem Rockafellar.theorem_3_6 {m p : ℕ} {C₁ C₂ : Set (TdafSurface.Rn m × TdafSurface.Rn p)} (h₁ : Convex ℝ C₁) (h₂ : Convex ℝ C₂) : Convex ℝ (partialAdd C₁ C₂)

Theorem 3.6. Let C₁ and C₂ be convex sets in ℝᵐ⁺ᵖ, and let C be the set of vectors x = (y, z) such that there exist z₁ and z₂ with (y, z₁) ∈ C₁, (y, z₂) ∈ C₂ and z₁ + z₂ = z. Then C is a convex set in ℝᵐ⁺ᵖ.

theorem Rockafellar.theorem_3_6_add {p : ℕ} (C₁ C₂ : Set (TdafSurface.Rn 0 × TdafSurface.Rn p)) : partialAdd C₁ C₂ = C₁ + C₂

Rockafellar, §3 (p. 20). Ordinary addition of convex sets in ℝⁿ is the extreme case m = 0 of Theorem 3.6.

theorem Rockafellar.theorem_3_6_inter {m : ℕ} (C₁ C₂ : Set (TdafSurface.Rn m × TdafSurface.Rn 0)) : partialAdd C₁ C₂ = C₁ ∩ C₂

Rockafellar, §3 (p. 20). Intersection of convex sets in ℝⁿ is the extreme case p = 0 of Theorem 3.6.

Theorem 3.7: the inverse sum

def Rockafellar.invSum {n : ℕ} (C₁ C₂ : Set (TdafSurface.Rn n)) : Set (TdafSurface.Rn n)

Rockafellar's inverse sum C₁ # C₂ = ⋃ {(1 - λ) C₁ ∩ λ C₂ | 0 ≤ λ ≤ 1}. The book obtains it as the partial addition "in the λ argument alone" of the cones in ℝⁿ⁺¹ corresponding to C₁ and C₂; that derivation is invSum_eq_partialAdd_coneLift.

Equations

• Rockafellar.invSum C₁ C₂ = ⋃ l ∈ Set.Icc 0 1, (1 - l) • C₁ ∩ l • C₂

theorem Rockafellar.mem_invSum {n : ℕ} {C₁ C₂ : Set (TdafSurface.Rn n)} {x : TdafSurface.Rn n} : x ∈ invSum C₁ C₂ ↔ ∃ (l : ℝ), 0 ≤ l ∧ l ≤ 1 ∧ x ∈ (1 - l) • C₁ ∧ x ∈ l • C₂

Membership in C₁ # C₂, with the union over λ ∈ [0, 1] unpacked.

theorem Rockafellar.mem_invSum_iff_exists {n : ℕ} {C₁ C₂ : Set (TdafSurface.Rn n)} {x : TdafSurface.Rn n} : x ∈ invSum C₁ C₂ ↔ ∃ (l : ℝ), 0 ≤ l ∧ l ≤ 1 ∧ ∃ x₁ ∈ C₁, ∃ x₂ ∈ C₂, x = (1 - l) • x₁ ∧ x = l • x₂

Rockafellar, §3 (p. 21). C₁ # C₂ consists of all the vectors x which can be expressed in the form x = (1 - λ) x₁ = λ x₂ with 0 ≤ λ ≤ 1, x₁ ∈ C₁ and x₂ ∈ C₂.

theorem Rockafellar.invSum_mono {n : ℕ} {C₁ C₂ D₁ D₂ : Set (TdafSurface.Rn n)} (h₁ : C₁ ⊆ D₁) (h₂ : C₂ ⊆ D₂) : invSum C₁ C₂ ⊆ invSum D₁ D₂

Inverse addition is monotone in both arguments.

theorem Rockafellar.invSum_eq_iUnion_singleton {n : ℕ} (C₁ C₂ : Set (TdafSurface.Rn n)) : invSum C₁ C₂ = ⋃ x₁ ∈ C₁, ⋃ x₂ ∈ C₂, invSum {x₁} {x₂}

Inverse addition is pointwise, C₁ # C₂ = {x₁ # x₂ | x₁ ∈ C₁, x₂ ∈ C₂}, in parallel with the formula for C₁ + C₂; {x₁} # {x₂} is non-empty exactly when x₁ and x₂ lie on a common ray through the origin.

theorem Rockafellar.invSum_singleton_smul {n : ℕ} (e : TdafSurface.Rn n) {a₁ a₂ : ℝ} (h₁ : 0 ≤ a₁) (h₂ : 0 ≤ a₂) : invSum {a₁ • e} {a₂ • e} = {(a₁ * a₂ / (a₁ + a₂)) • e}

The inverse sum of two vectors on a common ray: {α₁ e} # {α₂ e} = {[α₁α₂/(α₁+α₂)] e} for α₁, α₂ ≥ 0. The coefficient is stated as a product, not as the book's harmonic (α₁⁻¹+α₂⁻¹)⁻¹: since 0⁻¹ = 0 in Lean the harmonic form evaluates to α₂ at α₁ = 0, which is wrong, whereas the product form is correct throughout (0 / 0 = 0).

theorem Rockafellar.theorem_3_7 {n : ℕ} {C₁ C₂ : Set (TdafSurface.Rn n)} (h₁ : Convex ℝ C₁) (h₂ : Convex ℝ C₂) : Convex ℝ (invSum C₁ C₂)

Theorem 3.7. The inverse sum C₁ # C₂ of two convex sets is convex.

The cone correspondence behind inverse addition

def Rockafellar.coneLift {n : ℕ} (C : Set (TdafSurface.Rn n)) : Set (TdafSurface.Rn n × ℝ)

Rockafellar, §3 (p. 20). The convex cone in ℝⁿ⁺¹ associated with a convex set C in ℝⁿ: the one generated by {(x, 1) | x ∈ C}, written here with the height in the second coordinate so that partial addition in the height is partialAdd.

Equations

• Rockafellar.coneLift C = {q : TdafSurface.Rn n × ℝ | 0 ≤ q.2 ∧ q.1 ∈ q.2 • C}

@[simp]

theorem Rockafellar.mem_coneLift {n : ℕ} {C : Set (TdafSurface.Rn n)} {x : TdafSurface.Rn n} {l : ℝ} : (x, l) ∈ coneLift C ↔ 0 ≤ l ∧ x ∈ l • C

Membership in coneLift C, at an explicit pair: (x, λ) is in the cone exactly when λ ≥ 0 and x ∈ λ C.

theorem Rockafellar.coneLift_eq_iUnion_smul {n : ℕ} (C : Set (TdafSurface.Rn n)) : coneLift C = ⋃ l ∈ Set.Ici 0, l • (fun (x : TdafSurface.Rn n) => (x, 1)) '' C

coneLift C is exactly the union of the non-negative multiples of the cross-section {(x, 1) | x ∈ C}, which is why it deserves the name "the cone generated by" that section.

@[simp]

theorem Rockafellar.coneLift_section_one {n : ℕ} (C : Set (TdafSurface.Rn n)) : {x : TdafSurface.Rn n | (x, 1) ∈ coneLift C} = C

The cross-section of coneLift C at height 1 is C again: the correspondence C ↦ K of the book is one-to-one.

theorem Rockafellar.zero_mem_coneLift {n : ℕ} {C : Set (TdafSurface.Rn n)} (hne : C.Nonempty) : 0 ∈ coneLift C

coneLift C contains the origin of ℝⁿ⁺¹ whenever C is non-empty — the book's cones K are exactly the ones "containing the origin".

theorem Rockafellar.smul_mem_coneLift {n : ℕ} {C : Set (TdafSurface.Rn n)} {q : TdafSurface.Rn n × ℝ} (hq : q ∈ coneLift C) {c : ℝ} (hc : 0 ≤ c) : c • q ∈ coneLift C

coneLift C is closed under non-negative scaling.

theorem Rockafellar.convex_coneLift {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) : Convex ℝ (coneLift C)

coneLift C is a convex cone whenever C is convex. This, together with coneLift_eq_iUnion_smul, is the "convex cone K in ℝⁿ⁺¹ containing the origin and having a cross-section identifiable with C" of the book.

theorem Rockafellar.invSum_eq_partialAdd_coneLift {n : ℕ} (C₁ C₂ : Set (TdafSurface.Rn n)) : invSum C₁ C₂ = {x : TdafSurface.Rn n | (x, 1) ∈ partialAdd (coneLift C₁) (coneLift C₂)}

The inverse sum is the partial addition "in the λ argument alone" of coneLift C₁ and coneLift C₂, read off at height 1: the bridge between invSum and Theorem 3.6.

Theorem 3.8: cones

theorem Rockafellar.theorem_3_8_add {n : ℕ} {K₁ K₂ : Set (TdafSurface.Rn n)} (hc₁ : Convex ℝ K₁) (hc₂ : Convex ℝ K₂) (hs₁ : ∀ (c : ℝ), 0 < c → c • K₁ ⊆ K₁) (hs₂ : ∀ (c : ℝ), 0 < c → c • K₂ ⊆ K₂) (h0₁ : 0 ∈ K₁) (h0₂ : 0 ∈ K₂) : K₁ + K₂ = (convexHull ℝ) (K₁ ∪ K₂)

Theorem 3.8 (first equation). For convex cones K₁, K₂ containing the origin, K₁ + K₂ = conv (K₁ ∪ K₂).

theorem Rockafellar.theorem_3_8_invSum {n : ℕ} {K₁ K₂ : Set (TdafSurface.Rn n)} (hs₁ : ∀ (c : ℝ), 0 < c → c • K₁ ⊆ K₁) (hs₂ : ∀ (c : ℝ), 0 < c → c • K₂ ⊆ K₂) (h0₁ : 0 ∈ K₁) (h0₂ : 0 ∈ K₂) : invSum K₁ K₂ = K₁ ∩ K₂

Theorem 3.8 (second equation). For cones K₁, K₂ containing the origin, K₁ # K₂ = K₁ ∩ K₂. Stated without the convexity the book carries over from the first equation: closure under positive scaling and membership of the origin suffice.