Proper separation from a polyhedral set

Two nonempty convex sets separate properly exactly when their relative interiors are disjoint. When one of the two sets is polyhedral the relative interior on that side may be dropped, and the separating hyperplane can in addition be required not to contain the other set.

Main results

• exists_separates_not_subset_iff_disjoint_relint — a nonempty polyhedral C₁ and a nonempty convex C₂ separate by a hyperplane missing C₂ exactly when C₁ misses ri C₂ (Theorem 20.2 in [^1]).
• disjoint_relint_of_separates_of_not_subset — its easy half, which needs no polyhedrality.
• nonempty_inter_relint_iff_forall_supportFn — the same condition read through support functions.
• supportFn_le_neg_supportFn_neg_iff — the dictionary entry it rests on: δ*(y | s) is at most -δ*(-y | t) exactly when ⟨·, y⟩ is nowhere larger on s than it is on t.
• levelSet — the level set of a continuous linear functional, packaged as an affine subspace; it is what turns "constant on C" into "constant on aff C".

Implementation notes

The classical proof moves the common point of C₁ and the relative boundary of C₂' to the origin; here the translation stays explicit, so K is the cone generated by C₁ - x₀ and the subspace playing the role of M is M₀ = (aff C₂).direction ⊓ ker f. The half-space that works is found by a positivity argument rather than by elimination: pick any φ in the representation of C₁' with φ w > 0 at a point w of ri C₂' outside C₁'; for z ∈ C₂' the vector z - (f z / f w) • w lies in M₀, where φ vanishes, so φ z is a nonnegative multiple of φ w. Only the inclusion {y | y + x₀ ∈ aff C₂ ∧ f (y + x₀) > c} ⊆ ri C₂' is used, so no relative interior is computed.

References

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

def Tdaf.ConvexAnalysis.levelSet {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E →L[ℝ] ℝ) (c : ℝ) : AffineSubspace ℝ E

The level set {x | f x = c} of a continuous linear functional, as an affine subspace.

The only thing it is used for is affineSpan_le: a functional constant on a set is constant on the set's affine hull.

Equations

• Tdaf.ConvexAnalysis.levelSet f c = { carrier := {x : E | f x = c}, smul_vsub_vadd_mem' := ⋯ }

@[simp]

theorem Tdaf.ConvexAnalysis.mem_levelSet {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E →L[ℝ] ℝ} {c : ℝ} {x : E} : x ∈ levelSet f c ↔ f x = c

theorem Tdaf.ConvexAnalysis.forall_eq_of_mem_affineSpan {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E →L[ℝ] ℝ} {c : ℝ} {s : Set E} (h : ∀ x ∈ s, f x = c) (x : E) : x ∈ affineSpan ℝ s → f x = c

A continuous linear functional constant on a set is constant on its affine hull.

theorem Tdaf.ConvexAnalysis.disjoint_relint_of_separates_of_not_subset {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C₁ C₂ : Set E} {f : E →L[ℝ] ℝ} {c : ℝ} (hsep : Separates f c C₁ C₂) (hns : ¬C₂ ⊆ {x : E | f x = c}) : Disjoint C₁ (intrinsicInterior ℝ C₂)

The easy half, which needs no polyhedrality: a hyperplane separating C₁ and C₂ and not containing C₂ keeps C₁ out of ri C₂.

A point of C₁ ∩ ri C₂ would lie on the hyperplane, so -f would attain its maximum over C₂ at a relative interior point, forcing f to be constant on C₂.

theorem Tdaf.ConvexAnalysis.exists_separates_not_subset_iff_disjoint_relint {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C₁ C₂ : Set E} (h₁ : Polyhedral C₁) (h₂ : Convex ℝ C₂) (hne₂ : C₂.Nonempty) : (∃ (g : E →L[ℝ] ℝ) (c : ℝ), Separates g c C₁ C₂ ∧ ¬C₂ ⊆ {x : E | g x = c}) ↔ Disjoint C₁ (intrinsicInterior ℝ C₂)

Let C₁ be a nonempty polyhedral convex set and C₂ a nonempty convex set. Then C₁ and C₂ can be separated by a hyperplane which separates them properly and does not contain C₂, exactly when C₁ misses ri C₂.

The general criterion asks for ri C₁ ∩ ri C₂ = ∅ and promises nothing about containment: polyhedrality of C₁ buys both improvements at once. Properness of the separation is not stated separately — it follows from the non-containment of C₂.

The same condition through support functions

theorem Tdaf.ConvexAnalysis.supportFn_le_neg_supportFn_neg_iff {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (s t : Set E) (y : F) : supportFn B s y ≤ -supportFn B t (-y) ↔ ∀ x₁ ∈ s, ∀ x₂ ∈ t, (B x₁) y ≤ (B x₂) y

Separation, in support functions. The hyperplanes {x | ⟨x, y⟩ = α} that separate s from t are exactly those with δ*(y | s) ≤ α ≤ -δ*(-y | t); there is such an α exactly when the pairing with y is nowhere larger on s than on t.

Neither set has to be nonempty: an empty s sends the left side to ⊥ and an empty t sends the right side to ⊤, and both conditions are then vacuous.

theorem Tdaf.ConvexAnalysis.nonempty_inter_relint_iff_forall_supportFn {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {C₁ C₂ : Set E} [IsCompatiblePairing B] (h₁ : Polyhedral C₁) (hne₁ : C₁.Nonempty) (h₂ : Convex ℝ C₂) (hne₂ : C₂.Nonempty) : (C₁ ∩ intrinsicInterior ℝ C₂).Nonempty ↔ ∀ (y : F), supportFn B C₁ y ≤ -supportFn B C₂ (-y) → supportFn B C₁ y = supportFn B C₂ y

For a nonempty polyhedral C₁ and a nonempty convex C₂, C₁ meets ri C₂ exactly when every y for which some hyperplane ⟨·, y⟩ = α separates the two sets has δ*(y | C₁) = δ*(y | C₂) — that is, every separating hyperplane contains C₂.

This is the separation statement above with both sides negated and translated. It is the form the closedness criterion for C₁ + C₂ applies, to the barrier cones.