Rockafellar, §11: Separation Theorems

The three notions of separation, the fundamental separation construction, and supporting hyperplanes. All 16 numbered results of §11 are formalized, in the book's own vocabulary: a hyperplane is {x | ⟨x, b⟩ = β} with b ≠ 0, and separation is an inclusion of the two sets in the opposing closed half-spaces.

The section's definitions

• SeparatesRn b β C₁ C₂, SeparatesProperlyRn, SeparatesStrictlyRn, SeparatesStronglyRn — the section's four notions, each carrying b ≠ 0 so that {x | ⟨x, b⟩ = β} really is a hyperplane (Theorem 1.3). SeparatesStronglyRn is written as the book writes it, with Cᵢ + εB inside the open half-spaces; separatesStronglyRn_iff is the bridge to the backbone's gap definition, and is the substance of Theorem 11.1(c).
• SeparableProperly, SeparableStrongly — "there exists a hyperplane separating C₁ and C₂ properly / strongly", which is what every numbered result of the section is about.
• IsSupportingHalfSpace b β C — the supporting half-space, bridged to the backbone's IsSupporting by isSupportingHalfSpace_iff.

The book quantifies over vectors where the backbone quantifies over continuous linear functionals; TdafSurface.exists_linFn says the two are the same quantification in ℝⁿ, and every statement below is over vectors.

Which set lies on which side. Rockafellar's Theorem 11.1 puts C₁ in the upper half-space and C₂ in the lower one, where the backbone's Separates f c s t puts s below and t above. The definitions here therefore read Separates (linFn b) β C₂ C₁, so that the inequalities in every statement below are the book's.

corollary_11_5_2 and corollary_11_7_3 need C non-empty, where the book assumes only C ≠ ℝⁿ: in ℝ⁰ the empty set is a convex set other than ℝ⁰ and there is no non-zero b at all, so the conclusion fails. Every other §11 result carries the book's own non-emptiness hypothesis anyway.

References

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

Vectors as linear functions

linFn and exists_linFn live in TdafSurface/Common/Euclidean.lean; §§13, 14 and 18 want them too.

The four notions of separation (p. 95)

def Rockafellar.SeparatesRn {n : ℕ} (b : TdafSurface.Rn n) (β : ℝ) (C₁ C₂ : Set (TdafSurface.Rn n)) : Prop

Rockafellar, §11 (p. 95). The hyperplane H = {x | ⟨x, b⟩ = β}, b ≠ 0, separates C₁ and C₂: C₁ is contained in the closed half-space {x | ⟨x, b⟩ ≥ β} and C₂ in the opposite one. Recorded through the backbone's Separates, whose two sets go in the other order.

Equations

• Rockafellar.SeparatesRn b β C₁ C₂ = (b ≠ 0 ∧ Tdaf.ConvexAnalysis.Separates (TdafSurface.linFn b) β C₂ C₁)

def Rockafellar.SeparatesProperlyRn {n : ℕ} (b : TdafSurface.Rn n) (β : ℝ) (C₁ C₂ : Set (TdafSurface.Rn n)) : Prop

Rockafellar, §11 (p. 95). H separates C₁ and C₂ properly: it separates them, and they are not both actually contained in H itself.

Equations

• Rockafellar.SeparatesProperlyRn b β C₁ C₂ = (b ≠ 0 ∧ Tdaf.ConvexAnalysis.SeparatesProperly (TdafSurface.linFn b) β C₂ C₁)

def Rockafellar.SeparatesStrictlyRn {n : ℕ} (b : TdafSurface.Rn n) (β : ℝ) (C₁ C₂ : Set (TdafSurface.Rn n)) : Prop

Rockafellar, §11 (p. 95). H separates C₁ and C₂ strictly: the two sets belong to opposing open half-spaces. The book defines this notion and then numbers no result about it.

Equations

• Rockafellar.SeparatesStrictlyRn b β C₁ C₂ = (b ≠ 0 ∧ (∀ x ∈ C₂, ((TdafSurface.pairing n) x) b < β) ∧ ∀ x ∈ C₁, β < ((TdafSurface.pairing n) x) b)

def Rockafellar.SeparatesStronglyRn {n : ℕ} (b : TdafSurface.Rn n) (β : ℝ) (C₁ C₂ : Set (TdafSurface.Rn n)) : Prop

Rockafellar, §11 (p. 95). H separates C₁ and C₂ strongly: for some ε > 0, C₁ + εB is contained in one of the open half-spaces associated with H and C₂ + εB in the opposite one, where B is the closed Euclidean unit ball.

The book's definition verbatim; separatesStronglyRn_iff identifies it with the backbone's gap definition, which is condition (c) of Theorem 11.1.

Equations

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

theorem Rockafellar.separatesStronglyRn_iff {n : ℕ} {b : TdafSurface.Rn n} {β : ℝ} {C₁ C₂ : Set (TdafSurface.Rn n)} : SeparatesStronglyRn b β C₁ C₂ ↔ b ≠ 0 ∧ Tdaf.ConvexAnalysis.SeparatesStrongly (TdafSurface.linFn b) β C₂ C₁

The bridge for SeparatesStronglyRn: the book's εB definition is the backbone's gap ⨆_{C₂} ⟨·, b⟩ < β < ⨅_{C₁} ⟨·, b⟩. Specialises separatesStrongly_iff_exists_closedBall.

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

Rockafellar, §11. C₁ and C₂ can be separated properly: some hyperplane does it.

Equations

• Rockafellar.SeparableProperly C₁ C₂ = ∃ (b : TdafSurface.Rn n) (β : ℝ), Rockafellar.SeparatesProperlyRn b β C₁ C₂

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

Rockafellar, §11. C₁ and C₂ can be separated strongly: some hyperplane does it.

Equations

• Rockafellar.SeparableStrongly C₁ C₂ = ∃ (b : TdafSurface.Rn n) (β : ℝ), Rockafellar.SeparatesStronglyRn b β C₁ C₂

theorem Rockafellar.separableProperly_iff_exists {n : ℕ} {C₁ C₂ : Set (TdafSurface.Rn n)} (h₁ : C₁.Nonempty) (h₂ : C₂.Nonempty) : SeparableProperly C₁ C₂ ↔ ∃ (f : TdafSurface.Rn n →L[ℝ] ℝ) (c : ℝ), Tdaf.ConvexAnalysis.SeparatesProperly f c C₁ C₂

The bridge to the backbone for proper separability. Rockafellar's "there exists a hyperplane separating C₁ and C₂ properly" is the backbone's ∃ f c, SeparatesProperly f c C₁ C₂: the side-swap is SeparatesProperly.symm and b ≠ 0 is SeparatesProperly.ne_zero.

theorem Rockafellar.separableStrongly_iff_exists {n : ℕ} {C₁ C₂ : Set (TdafSurface.Rn n)} (h₁ : C₁.Nonempty) (h₂ : C₂.Nonempty) : SeparableStrongly C₁ C₂ ↔ ∃ (f : TdafSurface.Rn n →L[ℝ] ℝ) (c : ℝ), Tdaf.ConvexAnalysis.SeparatesStrongly f c C₁ C₂

The bridge to the backbone for strong separability, exactly as for proper separability.

Theorem 11.1

theorem Rockafellar.theorem_11_1_ab {n : ℕ} {C₁ C₂ : Set (TdafSurface.Rn n)} (h₁ : C₁.Nonempty) (h₂ : C₂.Nonempty) : SeparableProperly C₁ C₂ ↔ ∃ (b : TdafSurface.Rn n), ⨆ x ∈ C₂, ↑(((TdafSurface.pairing n) x) b) ≤ ⨅ x ∈ C₁, ↑(((TdafSurface.pairing n) x) b) ∧ ⨅ x ∈ C₂, ↑(((TdafSurface.pairing n) x) b) < ⨆ x ∈ C₁, ↑(((TdafSurface.pairing n) x) b)

Theorem 11.1, conditions (a) and (b). Let C₁ and C₂ be non-empty sets in ℝⁿ. There exists a hyperplane separating C₁ and C₂ properly if and only if there exists a vector b such that

(a) inf {⟨x, b⟩ | x ∈ C₁} ≥ sup {⟨x, b⟩ | x ∈ C₂}, and (b) sup {⟨x, b⟩ | x ∈ C₁} > inf {⟨x, b⟩ | x ∈ C₂}.

The extrema are taken in EReal, which removes the boundedness side conditions the book leaves implicit.

theorem Rockafellar.theorem_11_1_c {n : ℕ} {C₁ C₂ : Set (TdafSurface.Rn n)} (h₁ : C₁.Nonempty) (h₂ : C₂.Nonempty) : SeparableStrongly C₁ C₂ ↔ ∃ (b : TdafSurface.Rn n), ⨆ x ∈ C₂, ↑(((TdafSurface.pairing n) x) b) < ⨅ x ∈ C₁, ↑(((TdafSurface.pairing n) x) b)

Theorem 11.1, condition (c). There exists a hyperplane separating the non-empty sets C₁ and C₂ strongly if and only if there exists a vector b such that

(c) inf {⟨x, b⟩ | x ∈ C₁} > sup {⟨x, b⟩ | x ∈ C₂}.

The passage from Rockafellar's εB definition to this gap is separatesStronglyRn_iff, which is the substance of his proof.

Theorem 11.2, the fundamental construction

theorem Rockafellar.theorem_11_2 {n : ℕ} {C M : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hCne : C.Nonempty) (hCo : IsRelativelyOpen C) (hM : IsAffineSet M) (hMne : M.Nonempty) (hdisj : Disjoint C M) : ∃ (b : TdafSurface.Rn n) (β : ℝ), b ≠ 0 ∧ (∀ x ∈ M, ((TdafSurface.pairing n) x) b = β) ∧ ∀ x ∈ C, ((TdafSurface.pairing n) x) b < β

Theorem 11.2. Let C be a non-empty relatively open convex set in ℝⁿ, and let M be a non-empty affine set in ℝⁿ not meeting C. Then there exists a hyperplane H containing M, such that one of the open half-spaces associated with H contains C.

Stated for relatively open C and a general affine M, where the backbone has the open case and the single-point case.

Theorem 11.3, the main separation theorem

theorem Rockafellar.theorem_11_3 {n : ℕ} {C₁ C₂ : Set (TdafSurface.Rn n)} (h₁ : Convex ℝ C₁) (h₂ : Convex ℝ C₂) (hne₁ : C₁.Nonempty) (hne₂ : C₂.Nonempty) : SeparableProperly C₁ C₂ ↔ intrinsicInterior ℝ C₁ ∩ intrinsicInterior ℝ C₂ = ∅

Theorem 11.3. Let C₁ and C₂ be non-empty convex sets in ℝⁿ. In order that there exist a hyperplane separating C₁ and C₂ properly, it is necessary and sufficient that ri C₁ and ri C₂ have no point in common.

Theorem 11.4 and its corollaries

theorem Rockafellar.theorem_11_4_closure {n : ℕ} {C₁ C₂ : Set (TdafSurface.Rn n)} (h₁ : Convex ℝ C₁) (h₂ : Convex ℝ C₂) (hne₁ : C₁.Nonempty) (hne₂ : C₂.Nonempty) : SeparableStrongly C₁ C₂ ↔ 0 ∉ closure (C₁ - C₂)

Theorem 11.4, in the second of the two forms he gives it: strong separation of two non-empty convex sets is possible exactly when 0 ∉ cl (C₁ - C₂).

theorem Rockafellar.theorem_11_4 {n : ℕ} {C₁ C₂ : Set (TdafSurface.Rn n)} (h₁ : Convex ℝ C₁) (h₂ : Convex ℝ C₂) (hne₁ : C₁.Nonempty) (hne₂ : C₂.Nonempty) : SeparableStrongly C₁ C₂ ↔ ∃ ε > 0, ∀ x₁ ∈ C₁, ∀ x₂ ∈ C₂, ε ≤ ‖x₁ - x₂‖

Theorem 11.4. Let C₁ and C₂ be non-empty convex sets in ℝⁿ. In order that there exist a hyperplane separating C₁ and C₂ strongly, it is necessary and sufficient that inf {|x₁ - x₂| | x₁ ∈ C₁, x₂ ∈ C₂} > 0.

theorem_11_4_closure is the same statement written as 0 ∉ cl (C₁ - C₂), which is the form the backbone proves; a positive infimum of |x₁ - x₂| is exactly a ball around the origin missing C₁ - C₂.

theorem Rockafellar.corollary_11_4_1 {n : ℕ} {C₁ C₂ : Set (TdafSurface.Rn n)} (h₁ : Convex ℝ C₁) (hc₁ : IsClosed C₁) (hne₁ : C₁.Nonempty) (h₂ : Convex ℝ C₂) (hc₂ : IsClosed C₂) (hne₂ : C₂.Nonempty) (hdisj : Disjoint C₁ C₂) (hrec : Tdaf.ConvexAnalysis.recessionCone C₁ ∩ Tdaf.ConvexAnalysis.recessionCone C₂ ⊆ {0}) : SeparableStrongly C₁ C₂

Corollary 11.4.1. Let C₁ and C₂ be non-empty disjoint closed convex sets in ℝⁿ having no common directions of recession. Then there exists a hyperplane separating C₁ and C₂ strongly.

theorem Rockafellar.corollary_11_4_2 {n : ℕ} {C₁ C₂ : Set (TdafSurface.Rn n)} (h₁ : Convex ℝ C₁) (h₂ : Convex ℝ C₂) (hne₁ : C₁.Nonempty) (hne₂ : C₂.Nonempty) (hdisj : Disjoint (closure C₁) (closure C₂)) (hbdd : Bornology.IsBounded C₁ ∨ Bornology.IsBounded C₂) : SeparableStrongly C₁ C₂

Corollary 11.4.2. Let C₁ and C₂ be non-empty convex sets in ℝⁿ whose closures are disjoint. If either set is bounded, there exists a hyperplane separating C₁ and C₂ strongly.

A bounded closed set in ℝⁿ is compact; the book instead deduces this from Corollary 11.4.1.

Theorem 11.5 and its corollaries

theorem Rockafellar.theorem_11_5 {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hCc : IsClosed C) : ⋂ (b : TdafSurface.Rn n), ⋂ (β : ℝ), ⋂ (_ : ∀ y ∈ C, ((TdafSurface.pairing n) y) b ≤ β), {x : TdafSurface.Rn n | ((TdafSurface.pairing n) x) b ≤ β} = C

Theorem 11.5. A closed convex set C is the intersection of the closed half-spaces which contain it.

Indexed over vectors. The degenerate index b = 0 is harmless: {x | ⟨x, 0⟩ ≤ β} is ℝⁿ whenever β ≥ 0, the only case in which it contains a non-empty C.

theorem Rockafellar.corollary_11_5_1 {n : ℕ} (S : Set (TdafSurface.Rn n)) : ⋂ (b : TdafSurface.Rn n), ⋂ (β : ℝ), ⋂ (_ : ∀ y ∈ S, ((TdafSurface.pairing n) y) b ≤ β), {x : TdafSurface.Rn n | ((TdafSurface.pairing n) x) b ≤ β} = closure ((convexHull ℝ) S)

Corollary 11.5.1. Let S be any subset of ℝⁿ. Then cl (conv S) is the intersection of all the closed half-spaces containing S.

theorem Rockafellar.corollary_11_5_2 {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hne : C.Nonempty) (h : C ≠ Set.univ) : ∃ (b : TdafSurface.Rn n) (β : ℝ), b ≠ 0 ∧ ∀ x ∈ C, ((TdafSurface.pairing n) x) b ≤ β

Corollary 11.5.2. Let C be a convex subset of ℝⁿ other than ℝⁿ itself. Then there exists a closed half-space containing C; in other words, there exists some b ∈ ℝⁿ, b ≠ 0, such that the linear function ⟨·, b⟩ is bounded above on C.

C.Nonempty is added to the book's hypotheses — see the module docstring.

Theorem 11.6, supporting hyperplanes

def Rockafellar.IsSupportingHalfSpace {n : ℕ} (b : TdafSurface.Rn n) (β : ℝ) (C : Set (TdafSurface.Rn n)) : Prop

Rockafellar, §11 (p. 99). A supporting half-space to C is a closed half-space {x | ⟨x, b⟩ ≤ β}, b ≠ 0, which contains C and has a point of C in its boundary. The boundary {x | ⟨x, b⟩ = β} is then a supporting hyperplane to C.

Equations

• Rockafellar.IsSupportingHalfSpace b β C = (b ≠ 0 ∧ (∀ x ∈ C, ((TdafSurface.pairing n) x) b ≤ β) ∧ ∃ x ∈ C, ((TdafSurface.pairing n) x) b = β)

theorem Rockafellar.isSupportingHalfSpace_iff {n : ℕ} {b : TdafSurface.Rn n} {β : ℝ} {C : Set (TdafSurface.Rn n)} : IsSupportingHalfSpace b β C ↔ Tdaf.ConvexAnalysis.IsSupporting (TdafSurface.linFn b) β C

The bridge for IsSupportingHalfSpace: it is the backbone's IsSupporting for the functional ⟨·, b⟩.

theorem Rockafellar.theorem_11_6 {n : ℕ} {C D : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hD : Convex ℝ D) (hDC : D ⊆ C) (hDne : D.Nonempty) : (∃ (b : TdafSurface.Rn n) (β : ℝ), IsSupportingHalfSpace b β C ∧ (∀ x ∈ D, ((TdafSurface.pairing n) x) b = β) ∧ ∃ x ∈ C, ((TdafSurface.pairing n) x) b ≠ β) ↔ D ∩ intrinsicInterior ℝ C = ∅

Theorem 11.6. Let C be a convex set, and let D be a non-empty convex subset of C. In order that there exist a non-trivial supporting hyperplane to C containing D, it is necessary and sufficient that D be disjoint from ri C.

Stated with ri C, where the backbone has the interior version; a non-trivial supporting hyperplane to C through D is the same thing as a proper separation of D and C.

theorem Rockafellar.corollary_11_6_1 {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) {x : TdafSurface.Rn n} (hx : x ∈ C) (hfr : x ∈ frontier C) : ∃ b ∈ Tdaf.ConvexAnalysis.normalCone (TdafSurface.pairing n) C x, b ≠ 0

Corollary 11.6.1. A convex set has a non-zero normal at each of its boundary points.

Rockafellar's normal to C at x is the backbone's normalCone (pairing n) C x. Specialises exists_ne_zero_isMaxOn_of_mem_frontier.

theorem Rockafellar.corollary_11_6_2 {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) {x : TdafSurface.Rn n} (hx : x ∈ C) : x ∈ relbd C ↔ ∃ (b : TdafSurface.Rn n), (∀ y ∈ C, ((TdafSurface.pairing n) y) b ≤ ((TdafSurface.pairing n) x) b) ∧ ∃ y ∈ C, ((TdafSurface.pairing n) y) b ≠ ((TdafSurface.pairing n) x) b

Corollary 11.6.2. Let C be a convex set. An x ∈ C is a relative boundary point of C if and only if there exists a linear function h not constant on C such that h achieves its maximum over C at x.

relbd is §6's relative boundary.

Theorem 11.7, cones and homogeneous half-spaces

theorem Rockafellar.theorem_11_7 {n : ℕ} {C₁ C₂ : Set (TdafSurface.Rn n)} (hne₁ : C₁.Nonempty) (hne₂ : C₂.Nonempty) (hcone : IsCone C₂) (h : SeparableProperly C₁ C₂) : ∃ (b : TdafSurface.Rn n), SeparatesProperlyRn b 0 C₁ C₂

Theorem 11.7. Let C₁ and C₂ be non-empty subsets of ℝⁿ, at least one of which is a cone. If there exists a hyperplane which separates C₁ and C₂ properly, then there exists a hyperplane which separates C₁ and C₂ properly and passes through the origin.

Stated with the cone on the C₂ side; SeparatesProperlyRn b 0 C₁ C₂ says the separating hyperplane is {x | ⟨x, b⟩ = 0}, which contains the origin.

theorem Rockafellar.theorem_11_7' {n : ℕ} {C₁ C₂ : Set (TdafSurface.Rn n)} (hne₁ : C₁.Nonempty) (hne₂ : C₂.Nonempty) (hcone : IsCone C₁) (h : SeparableProperly C₁ C₂) : ∃ (b : TdafSurface.Rn n), SeparatesProperlyRn b 0 C₁ C₂

Theorem 11.7, with the cone on the C₁ side.

theorem Rockafellar.corollary_11_7_1 {n : ℕ} {K : Set (TdafSurface.Rn n)} (hconv : Convex ℝ K) (hcone : IsCone K) (hcl : IsClosed K) (hne : K.Nonempty) : ⋂ (b : TdafSurface.Rn n), ⋂ (_ : ∀ y ∈ K, ((TdafSurface.pairing n) y) b ≤ 0), {x : TdafSurface.Rn n | ((TdafSurface.pairing n) x) b ≤ 0} = K

Corollary 11.7.1. A non-empty closed convex cone in ℝⁿ is the intersection of the homogeneous closed half-spaces which contain it, a homogeneous half-space being one with the origin on its boundary.

theorem Rockafellar.corollary_11_7_2 {n : ℕ} (S : Set (TdafSurface.Rn n)) : ⋂ (b : TdafSurface.Rn n), ⋂ (_ : ∀ y ∈ S, ((TdafSurface.pairing n) y) b ≤ 0), {x : TdafSurface.Rn n | ((TdafSurface.pairing n) x) b ≤ 0} = closure ↑(PointedCone.hull ℝ S)

Corollary 11.7.2. Let S be any subset of ℝⁿ, and let K be the closure of the convex cone generated by S. Then K is the intersection of all the homogeneous closed half-spaces containing S.

The cone generated by S is PointedCone.hull ℝ S, which contains the origin; the book's own proof needs that, so no generality is lost.

theorem Rockafellar.corollary_11_7_3 {n : ℕ} {K : Set (TdafSurface.Rn n)} (hconv : Convex ℝ K) (hcone : IsCone K) (hne : K.Nonempty) (h : K ≠ Set.univ) : ∃ (b : TdafSurface.Rn n), b ≠ 0 ∧ ∀ x ∈ K, ((TdafSurface.pairing n) x) b ≤ 0

Corollary 11.7.3. Let K be a convex cone in ℝⁿ other than ℝⁿ itself. Then K is contained in some homogeneous closed half-space of ℝⁿ; in other words, there exists some vector b ≠ 0 such that ⟨x, b⟩ ≤ 0 for every x ∈ K.

K.Nonempty is added to the book's hypotheses, exactly as in Corollary 11.5.2.