Faces of a convex set #
A face of a convex set C is a convex subset C' of C such that every closed line segment
in C with a relative interior point in C' has both endpoints in C'. Everything here rests on
one strengthening of that definition: a face absorbs every convex subset of C whose relative
interior it meets. From it come the partition of C by the relative interiors of its faces and,
for compact C, Minkowski's theorem.
This file treats the bounded case, which is what the polyhedral theory and the Krein–Milman
corollaries consume. The representation of an unbounded closed convex set needs hulls of points
and directions (convexHullPD in HullDirections.lean) and lives in Representation.lean; the
exposed representation is in Exposed.lean and Tangent.lean.
Extreme points and exposed faces are Mathlib's Set.extremePoints and IsExposed;
isFace_singleton and IsExposed.isFace connect them to IsFace.
Main definitions #
Main results #
IsFace.subset_of_relint_inter_nonempty— a face absorbs every convex subset ofCwhose relative interior it meets (Theorem 18.1 in [^1]).IsFace.eq_inter_closure—C' = C ∩ cl C'; a face of a closed convex set is closed.IsFace.eq_of_relint_inter_nonempty— faces whose relative interiors meet are equal.IsFace.disjoint_relint,IsFace.subset_intrinsicFrontier,IsFace.finrank_vectorSpan_lt— a proper face lies in the relative boundary and has strictly smaller dimension.exists_isFace_subset_relint— every nonempty relatively open convex subset ofClies in the relative interior of a unique face ofC.exists_isFace_mem_relint,eq_iUnion_relint_isFace,IsFace.relint_pairwise_disjoint,IsFace.relint_maximal— the relative interiors of the nonempty faces partitionC, and are exactly the maximal relatively open convex subsets ofC(Theorem 18.2 in [^1]).exists_notMem_relint_mem_segment— in a compact set of positive dimension, every relative interior point lies on a segment joining two relative boundary points.convexHull_extremePoints— Minkowski's theorem: a compact convex set is the convex hull of its extreme points;extremePoints_nonemptyrecords that it has one.
References #
[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §18.
The definition and its elementary calculus #
Rockafellar's face: a convex subset C' of a convex set C such that every closed line
segment in C with a relative interior point in C' has both endpoints in C'. The segment
condition is exactly Mathlib's IsExtreme ℝ C C'; convexity of C' is a genuine extra
requirement, since {0, 1} is an extreme subset of [0, 1] but not a face of it.
- subset : C' ⊆ C
- left_mem_of_mem_openSegment ⦃x : E⦄ : x ∈ C → ∀ ⦃y : E⦄, y ∈ C → ∀ ⦃z : E⦄, z ∈ C' → z ∈ openSegment ℝ x y → x ∈ C'
A face is a convex set.
Instances For
Every convex set is a face of itself: the greatest element of the lattice of faces.
The empty set is a face of every set: the least element of the lattice of faces.
A face of a face is a face.
A face of C that happens to lie inside an intermediate convex set D is a face of D.
Cutting a face and its ambient set by the same convex set leaves a face. Note that D is
cut out of both sides, so this is not IsFace.inter, which intersects two faces of one set.
The intersection of a nonempty family of faces is a face. Together with Convex.isFace_self
and IsFace.empty this makes the faces of C a complete lattice under inclusion.
Rockafellar's extreme points are the zero-dimensional faces, so they are Mathlib's
Set.extremePoints.
Exposed faces are faces: the set on which a linear function attains its maximum over a
convex set C is a face of C. This is the only source of faces used in the partition theorem
below.
Mathlib's exposed faces are faces.
Faces absorb the convex subsets they meet #
A face absorbs every convex subset of C whose relative interior it meets. This
strengthens the defining segment property to arbitrary convex sets, and every other result in this
file goes through it. Convexity of D is not needed.
A face is cut out of C by its own closure. In particular a face of a closed convex set is
closed.
A face of a closed convex set is closed.
Two faces whose relative interiors have a point in common are equal. This is what makes the
relative interiors of the faces a partition of C.
A face other than C itself misses ri C.
A face other than C itself is contained in the relative boundary of C.
A face has the same affine hull as C only if it is all of C. This is the step from the
relative-boundary statement to the dimension statement.
The dimension statement: a nonempty face other than C itself has strictly smaller dimension
than C.
The relative interiors of the faces partition C #
The engine of the partition: every nonempty relatively open convex subset D of C lies in
the relative interior of a face of C, namely the smallest face containing D. Were D inside
the relative boundary of that face, a supporting hyperplane through D would cut out a strictly
smaller face still containing D.
The union half: every point of C is a relative interior point of some face of C.
The union half, as an equation.
The disjointness half: distinct faces have disjoint relative interiors.
The maximality half: the relative interior of a nonempty face is a maximal relatively open
convex subset of C.
The relative interior of a convex set is relatively open, so IsFace.relint_maximal really is
a maximality statement inside the family it quantifies over.
The bounded case: Minkowski's theorem #
For a compact set of positive dimension, a relative interior point lies on a segment joining
two points that are not relative interior points. The general statement asks instead that C be a
closed convex set which is neither an affine set nor a closed half of one; compactness is cruder
but is all Minkowski's theorem needs. Convexity of C is never used.
Minkowski's theorem: a closed bounded convex set is the convex hull of its extreme points.
It is the case of the general representation in which C has no directions of recession, and it is
stronger than Mathlib's Krein–Milman theorem (closure_convexHull_extremePoints), which gives only
the closed convex hull — the set of extreme points need not be closed even for a compact C. The
proof is an induction on dim C, through the partition of C by relative interiors of faces and
the segment lemma above.
A nonempty compact convex set has an extreme point: the convex hull of the empty set is empty.