Separation theorems #
Separation of convex sets by hyperplanes, over a real topological vector space — locally convex
where separation is actually invoked. Almost all of the mathematics is already in Mathlib, as the
geometric_hahn_banach_* family and iInter_halfSpaces_eq; what this file supplies is the
vocabulary — the three notions of separation, supporting hyperplanes and half-spaces — together
with the statements Mathlib does not have.
Two statements of the textbook are false at this generality and are corrected rather than
dropped. That a convex set other than the whole space lies in a closed half-space is proved there
through ri (cl C) ⊆ C, and fails in infinite dimensions: the kernel of a discontinuous linear
functional is a proper convex subset that is dense, so no nonzero continuous functional is bounded
above on it. The hypothesis here is closure s ≠ univ, and likewise for the cone version.
Proper separation by relative interiors, and the existence of a supporting hyperplane at every
relative boundary point, rest on the line segment principle and on ri C ≠ ∅ for nonempty convex
C; they are finite-dimensional and live in Tdaf/Analysis/Convex/RelativeInterior.lean.
Main definitions #
Separates f c s t— the hyperplane{x | f x = c}separatessandt:slies in the closed half-space{x | f x ≤ c}andtin the opposite one.SeparatesProperly f c s t— separation in whichsandtare not both contained in the hyperplane.SeparatesStrongly f c s t— separation with a gap:⨆_{s} f < c < ⨅_{t} f, the extrema being taken inEReal.IsSupporting f c s—{x | f x ≤ c}is a supporting half-space tosand{x | f x = c}a supporting hyperplane:f ≠ 0,f ≤ cons, andf x = csomewhere ons.halfSpaceCone f— the homogeneous closed half-space{x | f x ≤ 0}, bundled as aPointedCone ℝ E.
Main results #
separates_iff_iSup_le_iInf,exists_separatesProperly_iff_iSup_le_iInf,exists_separatesStrongly_iff_iSup_lt_iInf— the description of the three notions by the extrema offover the two sets (Theorem 11.1 in [^1]).separatesStrongly_iff_exists_gap,separatesStrongly_iff_exists_nhds,separatesStrongly_iff_exists_closedBall— the three faces of strong separation: a uniform gap, a neighbourhood of the origin, and — in a normed space — the textbook'sε-balls.exists_separates_of_isOpen_of_disjoint_affine— an open convex set and a disjoint affine set are separated by a hyperplane containing the affine set.separatesStrongly_iff_zero_notMem_closure_sub— strong separation is possible exactly when0 ∉ closure (s - t);separatesStrongly_of_disjoint_isCompact_isClosedis the compact/closed case.isClosed_convex_eq_iInter_halfspaces— a closed convex set is the intersection of the closed half-spaces containing it (Theorem 11.5 in [^1]), withmem_iff_forall_le_halfSpaceas its pointwise form andclosure_convexHull_eq_iInter_halfspacesfor an arbitrary set.exists_isSupporting_iff_disjoint_interior— a convex subset lies in a non-trivial supporting hyperplane exactly when it misses the interior.SeparatesProperly.zero_of_isCone_left— proper separation of a cone can always be moved to a hyperplane through the origin, whence the half-space representations of cones.exists_separating_of_notMem_closed_convex— the point/closed-convex-set case, in the form the conjugacy module consumes.exists_affine_lt_of_notMem,exists_affine_le_of_isClosed_epi— theE × ℝspecialisation: separating a point from a closed convex set that has a point vertically above it produces a non-vertical functional, hence a continuous affine function onE.
Implementation notes #
Strong separation is defined by the gap ⨆_{s} f < c < ⨅_{t} f rather than by the textbook's
C₁ + εB: the gap presupposes no topology on E, so its description by the extrema sits one layer
below the separation theorems that produce it, and taking the extrema in EReal removes the
Nonempty and BddAbove side conditions a real-valued sSup would force. Note that pointwise
strict separation — f < c on s and c < f on t — is a genuinely weaker notion and is not
among the three. General closed half-spaces are left as a pair (f, c), since the only facts ever
needed of {x | f x ≤ c} apply to that description directly; only the homogeneous ones are
bundled, as halfSpaceCone.
References #
[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §11.
The three notions of separation #
Separates f c s t : the hyperplane {x | f x = c} separates s and t, in the sense that
s lies in the closed half-space {x | f x ≤ c} and t in the opposite one. Rockafellar asks in
addition that f ≠ 0; that is not built in here, because it is automatic in the two notions where
it matters (SeparatesProperly.ne_zero, SeparatesStrongly.ne_zero).
fis at mostcons.fis at leastcont.
Instances For
SeparatesProperly f c s t : f separates s and t at level c, and s and t are not
both contained in the hyperplane {x | f x = c}. One of the two may be.
sandtdo not both lie inside the separating hyperplane.
Instances For
SeparatesStrongly f c s t : f separates s and t with a gap, the extrema being taken in
EReal so that empty and unbounded sets need no special treatment. Rockafellar's own definition
presupposes a norm, and is recovered by separatesStrongly_iff_exists_closedBall.
fstays bounded away fromcfrom below ons.fstays bounded away fromcfrom above ont.
Instances For
Separation passes to subsets.
Separation passes to closures: closed half-spaces are closed.
Separation passes to convex hulls: closed half-spaces are convex.
Proper separation is symmetric under exchanging the two sets and negating the functional.
A properly separating functional is nonzero, so that {x | f x = c} really is a hyperplane.
Separation and the extrema of a linear function #
The value of f at a point of s is at most the supremum of f over s. Spelling out the
indexed family is what keeps le_iSup₂ from having to guess it through a coercion.
The infimum of f over t is at most the value of f at a point of t.
Strong separation passes to subsets, exactly as ordinary separation does: shrinking the sets only shrinks the two extrema.
f separates s and t at level c exactly when c lies between the supremum of f over
s and its infimum over t.
The supremum of a real-valued function over a nonempty set is not ⊥.
The infimum of a real-valued function over a nonempty set is not ⊤.
Over a nonempty set the infimum is at most the supremum.
Some hyperplane orthogonal to f separates two nonempty sets exactly when f never exceeds on
s what it attains on t.
Proper separation is separation in which f dips strictly below c somewhere on s, or rises
strictly above it somewhere on t.
Two nonempty sets are properly separated by some hyperplane orthogonal to f exactly when f
never exceeds on s what it attains on t, and is not constant with one and the same value on
both.
Strong separation by some hyperplane orthogonal to f is exactly a gap between the two
extrema. No nonemptiness is needed here: for empty sets the extrema are ⊥ and ⊤.
Strong separation is separation.
On s, a strongly separating functional stays strictly below the level.
On t, a strongly separating functional stays strictly above the level.
Strong separation as a uniform gap. This is the form of Rockafellar's condition (c) that proofs actually consume.
The workhorse constructor for strong separation out of Mathlib's separation theorems, which
produce two levels u < v with f < u on s and v < f on t.
A strongly separating functional is nonzero, provided both sets are nonempty.
Strong separation is symmetric under exchanging the two sets and negating the functional.
Strong separation is proper, provided at least one of the two sets is nonempty.
Strong separation by a neighbourhood of the origin #
A nonzero continuous linear functional is strictly positive somewhere on every neighbourhood of
the origin. This is the substitute, in a space with no norm, for "|⟨y, b⟩| < δ for y small
enough".
A continuous linear functional that is nonpositive on a neighbourhood of the origin is zero.
A continuous linear functional attaining its maximum over a set at an interior point of that set is zero. This is what makes a supporting hyperplane at an interior point impossible.
Strong separation by a neighbourhood of the origin: the phrasing of Rockafellar's
definition that survives the loss of a norm. s + V and t + V lie in opposite open half-spaces
for some neighbourhood V of the origin.
A hyperplane through a disjoint affine set #
A continuous linear functional bounded below on an affine set is constant on it: along a
direction in which f decreases, an affine set is unbounded below for f.
An open convex set and a disjoint affine set can be separated by a hyperplane containing
the affine set, with the convex set inside one of the open half-spaces. Rockafellar's hypothesis
is that C be relatively open, which in ℝⁿ covers every nonempty convex set through ri C;
outside finite dimensions the relative interior is not available and openness is the right
hypothesis. The relatively open version is exists_lt_of_notMem_relint.
The same in the vocabulary of this file: an open convex set and a disjoint affine set are separated properly, by a hyperplane containing the affine set.
Supporting hyperplanes and half-spaces #
IsSupporting f c s : the closed half-space {x | f x ≤ c} is a supporting half-space to
s, and its boundary {x | f x = c} a supporting hyperplane — a closed half-space containing
s with a point of s in its boundary, f ≠ 0 making the boundary a hyperplane rather than the
whole space. A supporting hyperplane is non-trivial when ∃ x ∈ s, f x ≠ c, written inline.
A supporting hyperplane is a genuine hyperplane.
The half-space contains
s.- exists_eq : ∃ x ∈ s, f x = c
The hyperplane touches
s.
Instances For
A supporting hyperplane misses the interior of the set it supports.
A nonempty convex subset D of a convex set C with nonempty interior lies in a non-trivial
supporting hyperplane to C exactly when D misses the interior of C. Rockafellar's statement
is about ri C and needs no interior hypothesis, because in ℝⁿ a nonempty convex set has
nonempty relative interior; outside finite dimensions that fails. The relative-interior
consequences are in Tdaf/Analysis/Convex/RelativeInterior.lean.
Strong separation by ε-balls #
Rockafellar's own definition of strong separation, available once there is a norm: s + εB
and t + εB lie in opposite open half-spaces for some ε > 0. With
separatesStrongly_iff_exists_nhds this shows nothing is lost by taking the gap as the
definition.
Cones, and half-spaces through the origin #
The homogeneous closed half-space {x | f x ≤ 0}, bundled as a PointedCone ℝ E. The
homogeneous closed half-spaces — those with the origin on their boundary — are exactly these, and
bundling them makes Submodule.span_le available, which is what turns the cone representations
below into two lines.
Equations
Instances For
Membership in the homogeneous half-space cone is the inequality defining it.
The underlying set of halfSpaceCone f is the homogeneous half-space {x | f x ≤ 0}.
A linear functional bounded above on a cone is nonpositive on it: otherwise scaling up a point where it is positive breaks the bound.
A bound above for a linear functional on a nonempty cone is nonnegative: the functional comes
arbitrarily close to 0 along any ray of the cone.
If two nonempty sets are properly separated and the first is a cone, then they are properly
separated by a hyperplane through the origin. Both sets must be nonempty: on the line, the cone
{0} and the empty set are properly separated at level 1 but not at level 0.
The same with the cone on the right.
Strong separation, half-space representations, and separation from a point #
Two convex sets can be separated strongly exactly when the origin is not in the closure of their difference — in a normed space, exactly when the distance between them is positive. Rockafellar assumes both sets nonempty; that is not needed, the empty set being strongly separated from anything by the zero functional.
A compact convex set and a disjoint closed convex set can be separated strongly. The book deduces this from a criterion phrased with recession cones, which is not available yet; the proof here goes through Mathlib's compact/closed geometric Hahn–Banach theorem.
The other order: a closed convex set and a disjoint compact convex set can be separated strongly.
Separation of a point from a closed convex set, in the form the conjugacy module consumes: a point outside a closed convex set is separated from it strongly. This is the workhorse instance of the compact/closed case, and the only separation the Fenchel–Moreau theorem needs.
A point belongs to a closed convex set as soon as it satisfies every weak linear inequality that the set satisfies.
A closed convex set is the intersection of the closed half-spaces containing it.
The closed convex hull of an arbitrary set is the intersection of the closed half-spaces containing that set.
A nonempty convex set whose closure is not everything lies in a closed half-space, the
statement corrected for infinite dimensions. The book's hypothesis is C ≠ ℝⁿ, enough there
because ri (cl C) ⊆ C, but not here: the kernel of a discontinuous linear functional is a proper
convex subset which is dense, and no nonzero continuous functional is bounded above on it.
Corollaries 11.7.1 to 11.7.3 #
The closure of a cone is a cone.
A nonempty closed convex cone is the intersection of the homogeneous closed half-spaces containing it.
For an arbitrary set S, the closure of the convex cone generated by S is the intersection
of the homogeneous closed half-spaces containing S.
A nonempty convex cone whose closure is not everything is contained in a homogeneous closed
half-space, corrected for infinite dimensions exactly as
exists_ne_zero_forall_le_of_closure_ne_univ is.
The E × ℝ specialisation: non-vertical separation of an epigraph #
Separation in E × ℝ by a non-vertical functional. If (x₀, μ) ∉ F while (x₀, ν) ∈ F for
some ν > μ, the functional separating (x₀, μ) from the closed convex set F cannot be
vertical: a functional of the form (y, 0) takes the same value at (x₀, μ) and at (x₀, ν).
Normalising the vertical component to -1 turns it into a continuous affine function of E that
stays strictly below F and strictly above μ at x₀.
The epigraph form. A convex function with a closed epigraph has, at every point of its
domain and below every value it takes there, a continuous affine minorant passing above that value.
exists_affine_le_of_closed_proper is this lemma with μ := f x₀ - 1.