Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.
Closed convex hull and Straszewicz reductions #
This module packages the closed-convex-hull algebra and compact Krein-Milman/Straszewicz-style interfaces used in the Rockafellar 25.6 route.
If every point of s belongs to a closed convex set C, then the closed convex hull of s
is contained in C.
First inclusion in Rockafellar 25.6, in the local finite-valued setting.
If u is convex on domain, the sampling region lies in the interior of domain, and u is
continuous at the base point y, then the closed convex hull of gradient cluster values at y
is contained in the subdifferential at y.
Pointwise form of
closure_convexHull_gradientClusterSet_subset_subgradientOn_of_convexOn.
Open-domain version of the first inclusion in Rockafellar 25.6.
For a finite-dimensional finite-valued convex function on an open domain, continuity at interior
points and the inclusion sample ⊆ interior domain are automatic from sample ⊆ domain.
Pointwise open-domain version of the first inclusion in Rockafellar 25.6.
The closure of a set is contained in the closure of its convex hull.
A nonempty compact exposed face has an extreme point.
A nonempty compact exposed face contains a point which is extreme in the original set.
Compact Krein-Milman plus a Straszewicz-style exposed-point approximation hypothesis gives the closed-convex-hull exposed-point representation.
This theorem uses Mathlib's closure_convexHull_extremePoints and leaves only the
Straszewicz-type input explicit: every extreme point belongs to the closed convex hull of exposed
points. In Rockafellar 25.6 this compact form is one ingredient toward the no-lines closed
convex-set representation.
Compact Krein-Milman plus the literal Straszewicz-style exposed-point approximation hypothesis.
Here the hypothesis says every extreme point lies in the closure of exposed points, matching the
usual statement that every extreme point is a limit of exposed points. The previous
closed-convex-hull version follows because closure (exposedPoints s) is contained in
closure (convexHull ℝ (exposedPoints s)).
Compact Krein-Milman plus a Mathlib-shaped Straszewicz approximation hypothesis.
This variant accepts Mathlib's Set.exposedPoints notation directly and converts it to the
project-local inner-product exposed-point carrier.
Finite-dimensional compact-convex Straszewicz theorem, stated as a reusable theorem boundary.
This is the remaining convex-geometry input in the Rockafellar route: every extreme point of a compact convex set is a limit of Mathlib exposed points. It is stated separately from subdifferentials so the source-cube Aleksandrov theorem can depend on the standard compact-convex form rather than on an ad hoc subgradient-specific hypothesis.
Equations
- AleksandrovDifferentiability.StraszewiczCompactConvexStatement E = ∀ ⦃s : Set E⦄, IsCompact s → Convex ℝ s → Set.extremePoints ℝ s ⊆ closure (Set.exposedPoints ℝ s)
Instances For
If every extreme point is already exposed, then the Straszewicz closure conclusion is immediate.
In a subsingleton space, every point of every set is exposed in Mathlib's sense.
A singleton is exposed by the zero functional.
The compact-convex Straszewicz statement is trivial in a subsingleton ambient space.
The closure of the exposed points of a compact set is compact.
The weighted sum of a fixed finite tuple of points.
This is the continuous map from K^(n) times the standard simplex which will be used to prove
that finite-dimensional convex hulls of compact sets are compact.
Equations
- AleksandrovDifferentiability.convexCombinationTuple n xw = ∑ i : Fin n, xw.2 i • xw.1 i
Instances For
The fixed-tuple weighted-sum map is continuous.
A weighted tuple whose points lie in s and whose weights lie in the standard simplex gives a
point of convexHull ℝ s.
The image of K^n × Δⁿ under the weighted-tuple map is contained in convexHull ℝ K.
The fixed compact domain K^n × Δⁿ for the weighted-tuple map.
The fixed-tuple weighted-sum image of a compact set and the standard simplex is compact.
An affinely independent family in a finite-dimensional space can be indexed inside
Fin (finrank + 1).
This is the cardinality bridge used in the Carathéodory-to-fixed-simplex proof: after
Carathéodory gives an affinely independent family, this lemma provides room to pad it with zero
weights in the fixed index type Fin (Module.finrank ℝ E + 1).
Summing an extension-by-zero along an embedding recovers the original finite sum.
Padding scalar weights and points along an embedding with zero weights preserves the weighted sum.
In finite dimension, every point of convexHull ℝ s is represented by the fixed
(finrank + 1)-tuple weighted-sum image, provided s is nonempty.
This is Carathéodory's theorem plus the zero-padding bridge: Carathéodory gives an affinely
independent finite family of positive weights, the cardinality bound embeds that family into
Fin (finrank + 1), and all unused coordinates are filled by a base point of s with weight
zero.
For a nonempty set in finite dimension, the fixed (finrank + 1)-tuple simplex image is
exactly the convex hull.
In finite dimension, the convex hull of a compact set is compact.
In finite dimension, the convex hull of a compact set is closed.
For compact s in finite dimension, Rockafellar's
conv (closure exposedPoints) set is compact.
For compact s in finite dimension, Rockafellar's
conv (closure exposedPoints) set is closed.
Extreme points remain in the generating set when they lie in a convex hull inside the ambient convex set.
This is the compact-convex corollary used in Rockafellar's proof of Straszewicz's theorem: if
x is extreme in C, A ⊆ C, and x ∈ conv A, then x ∈ A. The proof is just extremeness
inherited by the smaller convex hull, followed by Mathlib's
extremePoints_convexHull_subset.
Contrapositive form of mem_of_mem_extremePoints_of_mem_convexHull_subset.
In Rockafellar's Straszewicz proof this is applied with A = closure S, where S is the exposed
point set: if the extreme point x is not in closure S, then it cannot lie in
conv (closure S).
Rockafellar's C₀ = conv (closure S) exclusion, specialized to exposed points.
If x is an extreme point of a closed convex set s but is not in the closure of the exposed
points of s, then x is not in the convex hull of that closure. This is the step in the
Straszewicz proof immediately before applying Hahn-Banach separation.
Compact version of
notMem_convexHull_closure_mathlib_exposedPoints_of_mem_extremePoints_of_notMem_closure.
Hahn-Banach separation in the exact compact Straszewicz setup.
If an extreme point of a compact convex set is not in the closure of the exposed points, then it is
strictly separated from conv (closure exposedPoints). This is the separation step in
Rockafellar's proof, with the closedness supplied by finite-dimensional compact convex-hull
compactness rather than left as an assumption.
The abstract exposed-point reduction behind Rockafellar 25.6.
If all points of s are in the closed convex hull of the exposed points of s, and every exposed
point of s belongs to a closed convex set C, then all points of s belong to C.
For the subgradient cluster-density theorem, s is the subdifferential at a fixed point and
C is the closed convex hull of nearby gradient cluster values. Rockafellar's closed-convex-set
structure theorem and Straszewicz's theorem supply the first hypothesis; the exposed-point
outer-semicontinuity argument supplies the second.