Internal representation of a closed convex set #
The theorems that recover a closed convex set from its extremal structure: once it contains no
line it is the convex hull of its extreme points and extreme directions, its faces are themselves
such hulls, and its exposed points are dense in its extreme points. Face.lean supplies the faces
themselves, and HullDirections.lean supplies convexHullPD, the convex hull of a set of points
together with a set of directions, which is what "C = conv S" means once S may contain
directions. The exposed representation is in Exposed.lean.
Main definitions #
ContainsNoLine C— no line is contained inC; Rockafellar's "Ccontains no lines".IsExtremeDirection C y— the direction ofyis an extreme direction ofC: some closed half-line in the direction ofyis a face ofC.extremeDirections Cis the set of suchy.IsAffineHalf C—Cis an affine set or a closed half of one: the intersection ofaff Cwith a closed half-space. Allowing the functional to vanish makes the affine case the caseφ = 0, so the two exceptional families of the segment theorem below become one predicate.
Main results #
exists_notMem_relint_mem_segment_of_not_isAffineHalf— in a closed convex set that is neither an affine set nor a closed half of one, every relative interior point lies on a segment joining two relative boundary points (Theorem 18.4 in [^1]). The analytic core isexists_notMem_relint_mem_segment_of_isBounded, the geometric inputexists_notMem_relint_mem_segment_of_not_convex, andisAffineHalf_of_convex_sdiff_relintidentifies the exceptions.convexHullPD_extremePoints_extremeDirections— the Minkowski–Klee representation: a closed convex set containing no lines is the convex hull of its extreme points and extreme directions (Theorem 18.5 in [^1]).extremePoints_nonempty_of_containsNoLineextracts an extreme point,coneHull_extremeDirections_eqandconeHull_of_forall_extremeDirectiontreat cones, and Minkowski's theorem for compact sets isconvexHull_extremePointsinFace.lean, used here as the base case of the induction.isFace_recessionCone— the recession cone of a face is a face of the recession cone, given that it is contained in it.extremeDirections_subset_extremeDirections_recessionConeis the consequence for extreme directions;isExtremeDirection_recessionConeneeds no topology.isFaceEquivInter— the face correspondence: forNa subspace of the lineality space ofCandMa complement ofN, the faces ofCcorrespond one-to-one with the faces ofC ∩ M. The mechanism isIsFace.linealitySpace_subset: a face is linear in every direction in whichCis.IsFace.eq_convexHullPD— a nonempty face ofconv Sis the hull of the points ofSit contains and the directions ofSin which it recedes.extremePoints_convexHullPD_subsetandexists_mem_eq_smul_of_mem_extremeDirectionsare the two corollaries — every extreme point is a generating point, every extreme direction a generating direction — andfinite_extremePoints_convexHullPDthe counting corollary a finitely generated set wants.containsNoLine_inter_of_isCompl— intersecting a closed convex set with a complement of its lineality space leaves a set containing no lines. Witheq_add_inter_of_isComplthis is the reduction of a general closed convex set to a line-free one.extremePoints_subset_closure_exposedPoints— Straszewicz's theorem: the exposed points of a closed convex set are dense in its extreme points (Theorem 18.6 in [^1]); Mathlib does not have this.mem_exposedPoints_of_forall_norm_sub_leis the geometric heart (a farthest point is exposed) andclosure_convexHull_exposedPointsthe representationC = cl (conv (exp C)).
Implementation notes #
The description of a face of conv S avoids the appeal to the prolongation principle — which
would need the positive-coefficient description of ri (conv S) — by splitting the generating
points into those inside the face and those outside (IsExtreme.mem_convexHull_inter) and handling
the directions by an induction over the cone hull. The induction proving the Minkowski–Klee
representation splits on finrank ℝ (vectorSpan ℝ C): dimension ≤ 1 is settled by
exists_eq_halfLine, the bounded case in every dimension by Minkowski's theorem, and only the
unbounded case of dimension ≥ 2 uses the segment theorem. Straszewicz is proved in a Euclidean
space, its farthest-point construction being inner-product geometry, and transported to a general
finite-dimensional normed space through toEuclidean.
References #
[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §18.
Lines, extreme directions, and half-line faces #
C contains no line: no full line lies in C. This is the standing hypothesis of the
extreme and exposed representation theorems. For a nonempty closed convex set it says that the
lineality space is trivial (containsNoLine_iff_linealitySpace_eq_zero), but unlike that
formulation it is also correct for C = ∅.
Instances For
A subset of a set containing no line contains no line.
The empty set contains no lines.
y generates an extreme direction of C: y ≠ 0 and some closed half-line in the
direction of y is a face of C. Rockafellar's extreme direction is the direction of such a
half-line face; representing it by a generating vector avoids a quotient, at the cost of the set
extremeDirections C being closed under multiplication by positive scalars.
Equations
- Tdaf.ConvexAnalysis.IsExtremeDirection C y = (y ≠ 0 ∧ ∃ (x : E), Tdaf.ConvexAnalysis.IsFace C (Tdaf.ConvexAnalysis.halfLine x y))
Instances For
The set of vectors that generate extreme directions of C.
Equations
Instances For
Membership in extremeDirections, unfolded.
Extreme directions do not change under positive rescaling of the generator.
An extreme direction of a face of C is an extreme direction of C: this is IsFace.trans.
The half-line in an extreme direction lies in C.
The recession cone of a half-line is the half-line in the same direction issuing from the
origin. A restatement of recessionCone_halfLine, which produces the ray as a set-builder.
The recession cone of a face is a face of the recession cone. The inclusion 0⁺C' ⊆ 0⁺C is
genuinely a hypothesis: the recession cone is not monotone in general, and for a nonempty subset of
a closed convex set it comes from the description of recession by unbounded directions. Everything
else is algebraic — no topology, no convexity of C, no nonemptiness. The case that matters is a
half-line face: if C' has endpoint x, then C' - x is an extreme ray of 0⁺C.
An extreme direction in which C recedes is an extreme direction of 0⁺C. The half-line
face x + ℝ₊ y of C becomes the half-line face ℝ₊ y of 0⁺C, an extreme ray of that cone. The
hypothesis y ∈ 0⁺C is automatic for a closed convex C; assuming it directly keeps the statement
free of topology.
Faces and the lineality space #
A face is linear in every direction in which the ambient set is linear. For y in the
lineality space of C and x in a face C', the segment from x - y to x + y lies in C and
has x as its midpoint, so both endpoints lie in C'. This is what makes Rockafellar's reduction
of the facial structure to lineality zero work: a face of C is a union of translates of the
lineality space.
A face inherits Rockafellar's direct-sum decomposition. If N is a subspace of the
lineality space of C and M is a complement of N, then every face C' of C splits as
N + (C' ∩ M). This is eq_add_inter_of_isCompl_of_le applied to C', which is legitimate
because a face absorbs the lineality of C.
Adding a complemented subspace back is undone by cutting with the complement. For
C₀ ⊆ M and M a complement of N, (N + C₀) ∩ M = C₀.
A face of the reduced set generates a face of the whole set. If N is a subspace of the
lineality space of C, M a complement of N, and C₀ a face of C ∩ M, then N + C₀ is a
face of C. With IsFace.inter_convex and IsFace.eq_add_inter_of_isCompl_of_le this is
Rockafellar's remark that the faces of C correspond one-to-one with those of C ∩ L^⊥; the
inverse pair is packaged as isFaceEquivInter.
The face correspondence: for N a subspace of the lineality space of C and M a
complement of N, the faces of C are in one-to-one correspondence with the faces of C ∩ M, by
C' ↦ C' ∩ M and C₀ ↦ N + C₀. Rockafellar takes N the full lineality space L and M = L^⊥
in ℝⁿ; every subspace of L and every complement of it works, and no closedness or
finite-dimensionality is used.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Extreme points of a subset #
An extreme point of C that happens to lie in a subset K of C is an extreme point of K.
Extremality only becomes harder to satisfy as the ambient set grows.
An extreme set absorbs the vertices of a convex combination it contains. If u lies in an
extreme subset C' of C and is a convex combination of points of P ⊆ C, then u is already a
convex combination of those points of P that lie in C'. This is the mechanism behind the
description of a face of a hull below; the textbook argument instead puts u in the relative
interior of the hull of the points actually used.
Convex cones, and the extreme points and directions of a hull #
A convex set closed under multiplication by non-negative scalars is closed under
addition: u + v is twice the midpoint of u and v.
The cone hull of a subset of a convex cone stays inside it. The cone K is described by
the two properties Rockafellar uses — convexity and closure under non-negative scalar
multiplication — rather than as a bundled PointedCone.
The origin is the only extreme point of a cone containing no lines. The half needing the no-lines hypothesis is that the origin is extreme: a segment through the origin with endpoints in a cone spans a whole line inside that cone.
Every extreme point of a hull of points and directions is one of its points. It can be deduced from the description of a face of such a hull by taking the face to be a single point; directly, a nonzero direction of recession at an extreme point would place that point strictly inside a segment.
A hull of finitely many points and directions has finitely many extreme points. Immediate
from extremePoints_convexHullPD_subset, which puts every extreme point among the generating
points.
Faces and directions of recession #
Splitting off a direction of recession at a point of a face. If a point x of the face
C' is obtained from a point w of C by adding a direction of recession v of C, then both
w and x + v lie in C', because x is the midpoint of the segment from w to x + v.
Iterating IsFace.mem_and_add_mem: the face contains every point x + n * t • y.
A line inside a convex set is a line of directions in the lineality space.
"Contains no line" is lineality zero, for a nonempty closed convex set.
Intersecting a closed convex set with a complement of its lineality space kills every line.
This is what makes the direct-sum decomposition C = L + (C ∩ N) useful: the second summand is a
set to which every theorem carrying a "contains no lines" hypothesis applies. A line in C ∩ N has
direction in L, is also a difference of two points of N, and L ⊓ N = ⊥.
An extreme direction is a direction of recession: a closed convex set recedes in every direction in which it contains a half-line.
Every extreme direction of a closed convex set is an extreme direction of its recession
cone. This sharpens extremeDirections_subset_recessionCone, which says only that an extreme
direction is a direction of recession. The converse fails: a parabolic region in the plane has no
half-line faces at all, while its recession cone is a ray.
Relatively open closed convex sets are affine #
A closed convex set that coincides with its relative interior contains whole lines. If
C ⊆ ri C then, for every x ∈ C and every direction d of the affine hull, the entire line
x + ℝ d lies in C. This is what makes the exceptional sets below exceptional.
A closed convex set that coincides with its relative interior is an affine set.
Relative interior points on segments between relative boundary points #
The analytic core of the segment theorem. If the line through a relative interior point x
of a closed set C, in a direction of the affine hull of C, meets C in a bounded set, then x
lies on a segment joining the two ends of that intersection, neither of which is a relative
interior point. Convexity of C is not used.
The segment theorem in the form the proof produces: if the relative boundary of a closed
convex set C is not convex, then every relative interior point of C lies on a segment joining
two relative boundary points. Rockafellar's own hypothesis — that C is neither an affine set nor
a closed half of one — is equivalent; see exists_notMem_relint_mem_segment_of_not_isAffineHalf.
Non-convexity of the relative boundary produces two relative boundary points whose segment meets
ri C; the line through them meets C in exactly that segment, by the line segment principle, so
every parallel line meets C in a bounded set.
Affine sets and closed halves of affine sets #
C is an affine set or a closed half of an affine set: the intersection of its own affine
hull with a closed half-space. The two exceptional cases of the segment theorem are one predicate
here, because the degenerate choice φ = 0, α = 0 gives exactly the affine sets.
Equations
Instances For
An affine set is a (degenerate) closed half of an affine set.
The exceptional sets are exactly those whose relative boundary is convex. If the relative
boundary of a closed convex set C is convex, then C is an affine set or a closed half of one.
A supporting hyperplane at a relative interior point of the relative boundary contains the whole
relative boundary, ri C lies strictly on one side, and every point of aff C strictly on that
side already lies in C.
The segment theorem: if a closed convex set is neither an affine set nor a closed half of an affine set, then each of its relative interior points lies on a line segment joining two relative boundary points.
An affine set, or a closed half of an affine set, of dimension at least two contains a
line. This is why the segment theorem applies to every closed convex set of dimension at least
two that contains no lines, and hence why the induction below only has to treat dimensions 0 and
1 separately.
Half-lines: the one-dimensional unbounded case #
The endpoint of a closed half-line is an extreme point of it.
The direction of a closed half-line is an extreme direction of it: the half-line is a face of itself.
A closed half-line is the convex hull of its unique extreme point and its unique extreme direction.
The faces of a hull of points and directions #
A direction of recession of C that carries a point of C into the face C' is a direction
of recession of C' itself. This is the delicate step: the face contains a whole half-line in that
direction, so cl C' recedes in it, and a face is the trace on C of its own closure.
A face of a convex hull of points and directions is itself the convex hull of the points it contains and the directions in which it recedes.
If no half-line meets the points of S in an unbounded set, then every extreme direction of
conv S is the direction of one of the vectors of S.
The same under the hypothesis Rockafellar highlights: if the points of S form a bounded set,
every extreme direction of conv S is the direction of a vector of S.
The Minkowski–Klee representation #
An unbounded closed convex set of dimension at most one that contains no line is a closed half-line. This is the only case the induction below cannot reduce, and it is trivial.
The representation for bounded sets: Minkowski's theorem, convexHull_extremePoints, with
the extreme directions (of which there are none) carried along.
The representation in dimension ≤ 1: C is empty, a point, a segment, or a half-line.
The Minkowski–Klee representation: a closed convex set containing no lines is the convex
hull of its extreme points and extreme directions. The proof is an induction on dim C: for a set
of dimension at least two the relative boundary is not convex, so every relative interior point
lies on a segment joining two relative boundary points, and each of those lies in the relative
interior of a face of strictly smaller dimension, again closed and line-free. Dimensions 0 and
1 are the base cases: a bounded set by Minkowski's theorem, an unbounded one a half-line.
A nonempty closed convex set containing no lines has at least one extreme point: a hull of directions alone would be empty.
A closed convex cone containing no lines is the cone generated by its extreme directions.
The version for an arbitrary set of generators of the extreme rays follows by monotonicity of the
cone hull; it is coneHull_of_forall_extremeDirection below.
The same for an arbitrary generating set: if every extreme ray of a closed convex cone C
containing no lines is generated by some vector of a subset T of C, then T generates C.
Rockafellar assumes the cone contains more than the origin; that is unnecessary, since the zero
cone has no extreme directions and both sides are {0}.
Straszewicz's theorem, the Euclidean core #
A farthest point is an exposed point. If p ∈ C maximises the distance to y over C,
then p is an exposed point of C: the linear functional ⟪p - y, ·⟫ attains its maximum over
C at p and nowhere else. Geometrically, the sphere about y through p contains C, and the
tangent hyperplane to that sphere at p meets it only at p. Neither convexity nor closedness of
C is needed.
Transport of exposed points along a linear homeomorphism #
Exposed points are preserved by a linear homeomorphism. The Mathlib counterpart for extreme
points is image_extremePoints; the proof here is the same idea, composing the exposing functional
with the inverse map.
Straszewicz's theorem in a general finite-dimensional space #
Exposedness is a local property of a convex set. A point exposed in the truncation
C ∩ closedBall c r that lies in the open ball is already exposed in C.
This is the reduction of Straszewicz's theorem to the bounded case.
A nonempty compact set in a finite-dimensional real normed space has an exposed point.
Straszewicz's theorem for a compact convex set: every extreme point is a limit of exposed points.
Straszewicz's theorem. For a closed convex set C, every extreme point of C is a limit
of exposed points of C. Together with Set.exposedPoints_subset_extremePoints this says that the
exposed points of C form a dense subset of its extreme points.
Straszewicz's theorem, in the form "the exposed points and the extreme points of a closed convex set have the same closure".
Straszewicz's theorem in representation form: a compact convex set is the closed convex hull of its exposed points. The closure cannot be dropped — the exposed points of a compact convex set need not be closed — which is why the exposed representation carries a closure where the extreme representation does not.