Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.
Convex subgradients #
This file records the project-local subgradient predicate for real-valued convex functions on an inner product space.
A uniform closed-ball estimate is preserved by convex combinations and by taking closure.
This is the elementary closed-convex-hull step used in the source proof when passing from limits
of gradients at differentiability points to arbitrary subgradients. The separate convex-analysis
density theorem should provide the hypothesis p ∈ closure (convexHull ℝ s).
Image form of norm_sub_le_of_mem_closure_convexHull_norm_sub_le.
This is the form used in the subgradient-extension step: once a convex-analysis density theorem places a subgradient in the closed convex hull of nearby gradient values, any uniform norm estimate on those gradient values passes to the subgradient.
Closed-convex-hull membership from all closed halfspace tests.
This is the separation-theorem half of the remaining finite-dimensional subgradient cluster-density input. To prove that a subgradient lies in the closed convex hull of cluster gradients, it is enough to show that every linear inequality true on the cluster gradients is true for the subgradient.
p is a subgradient of u at x, relative to the set s.
This is the supporting-hyperplane-from-below formulation used in the convex specialization of the Aleksandrov proof.
Equations
Instances For
The subgradients of u at a fixed point form a convex set.
Set-valued form of convexity of the subdifferential at a fixed point.
The subdifferential at a fixed point is closed.
If x ∉ s, the subdifferential is empty. If x ∈ s, it is the intersection over y ∈ s of
the closed half-spaces expressing the supporting inequalities.
Closed-graph form of the subgradient inequality along a convergent filter.
If base points xs converge to x, slopes ps converge to p, the function values
u (xs i) converge to u x, and eventually ps i is a subgradient at xs i, then p is a
subgradient at x. This is the local finite-valued version of the closedness of the
subdifferential graph used in Rockafellar 25.6.
Closed-graph form of the subgradient inequality when continuity of u at the limit point
supplies convergence of the function values.
A bounded subdifferential is compact in a proper space.
For the finite-dimensional endpoint-attainment argument, ProperSpace E is supplied by
finite-dimensionality. The separate convex-analysis input is local boundedness of subgradients.
A bounded nonempty subdifferential has a maximizer for every directional pairing.
A bounded nonempty subdifferential has a minimizer for every directional pairing.
First-order linearization of all nearby subgradients.
The two set parameters intentionally play different roles. In the source proof, subgradients are
taken relative to the larger convex domain Q_3, while the base point is approached through the
smaller working region Q_{3/2}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Extend subgradient linearization from a punctured approach set to the full approach set when the base-point subgradients are all equal to the model slope.
Cluster values of an auxiliary slope map G along the differentiability/approach set D.
In the source proof, G is the Fréchet gradient and D is the set of differentiability points.
Thus GradientClusterSet D G y is the set of all limits of gradients along points
w ∈ D with w -> y.
Equations
Instances For
Enlarging the approach set enlarges the gradient cluster set.
Closed-convex-hull membership of gradient cluster values is monotone in the approach set.
A point of the approach set contributes its own value as a cluster value.
This uses the non-punctured ambient filter 𝓝[D] y: the point y itself belongs to every
neighborhood within D, so no continuity of G is required.
A genuine limit along the within-filter is, in particular, a cluster value.
This is the filter-level form of the exposed-point step in Rockafellar 25.6: once nearby differentiability gradients are shown to converge to an exposed subgradient, that subgradient belongs to the corresponding gradient cluster set.
If G is eventually in every ball around q along the within-filter, then q is a cluster
value.
Norm-estimate version of GradientClusterSet.mem_of_eventually_mem_ball.
This is the final metric step in the exposed-point part of Rockafellar 25.6: once
outer semicontinuity forces nearby differentiability gradients to satisfy
‖G w - q‖ < ε for every ε > 0, the exposed subgradient q is a gradient cluster value.
A point of the approach set belongs to the closed convex hull of the corresponding cluster-value set through its own value.
A cluster value along a parameterization whose image tends to y through D is an ambient
gradient cluster value at y.
Cluster values along an affine line, restricted to parameters whose images lie in D, are
ambient gradient cluster values.
Positive-line version of GradientClusterSet.mem_of_lineMapClusterPt.
Cluster-density from halfspace tests on the gradient cluster set.
This is the separation reduction for the remaining convex-analysis input: to prove a subgradient belongs to the closed convex hull of the gradient cluster values, it suffices to prove every linear upper bound valid for all cluster values is valid for that subgradient.
Eventual version of the halfspace-test reduction for the subgradient cluster-density hypothesis used in the Aleksandrov proof.
Short alias for the halfspace-test form of the subgradient cluster-density hypothesis.
A directional cluster value dominating p transfers cluster halfspace bounds to p.
Directional dominating cluster values imply the halfspace-test form of cluster density.
Eventual version of
HasSubgradientLinearizationOnAt.clusterHalfspace_of_forall_exists_cluster_inner_ge.
Directional dominating cluster values imply the closed-convex-hull cluster-density hypothesis used by the Aleksandrov proof.
Eventual estimates for nearby gradient values pass to cluster gradient values.
This is the formal closed-set passage in the source proof: after proving an estimate for
G w for all w sufficiently close to y through D, the same estimate holds for every
cluster value q = lim G w.
Closed-convex-hull transfer from cluster gradients to all nearby subgradients.
This is the source subgradient-extension argument after the finite-dimensional density theorem: if every nearby subgradient belongs to the closed convex hull of the gradient cluster set, and the cluster gradients satisfy the linearization estimate, then all nearby subgradients satisfy the same estimate.
Source-shaped subgradient extension using cluster gradients.
This combines the closed-set passage to cluster gradient values with the closed-convex-hull density input for subgradients.
Punctured source-shaped subgradient extension using cluster gradients, with the base point
handled separately by uniqueness of the subgradient at x.
Convert a gradient little-o expansion at x into the moving-base estimates used by the
cluster-gradient subgradient extension.
For a nearby point y ≠ x, the estimate for G w - p₀ - B (w - x) is applied with
w -> y through D, while continuity of B controls the replacement of B (w - x) by
B (y - x).
Closed-convex-hull transfer principle for subgradient linearization.
This isolates the elementary part of the source subgradient-extension lemma. If every nearby subgradient lies in the closed convex hull of auxiliary slopes, and those auxiliary slopes satisfy the desired first-order estimate, then every nearby subgradient satisfies the same estimate. The remaining source input is the convex-analysis theorem producing the closed-convex-hull inclusion from gradients at nearby differentiability points.
Convert a gradient expansion at the base point into the moving-base slope estimates needed by the closed-convex-hull subgradient transfer.
The family t y should be read as the differentiability sample points approaching y. The
hypothesis hwithin says that, as y -> x through approach, all points of t y eventually lie
in every neighborhood of x inside D. The estimate hBsmall is the formal version of the
source proof's passage from B (w - x) to B (y - x) when w -> y.
Source-shaped subgradient extension from a gradient little-o expansion plus a closed-convex hull density input.
This packages the proof of the source lemma up to the finite-dimensional density theorem: the gradient expansion gives the moving-base estimates on nearby differentiability samples, and the closed-convex-hull transfer then extends the estimate to every nearby subgradient.
Evaluate a subgradient-linearization estimate along increment coordinates.
This is the form used in the final Taylor step: if small increments z keep x + z inside the
approach set, then the model estimate can be written with displacement z rather than
(x + z) - x.
Uniform segment form of eventually_increment_estimates.
This matches the source proof's final integration step: after shrinking z, every point
x + t • z, 0 ≤ t ≤ 1, lies in the approach set and in the neighborhood where the
subgradient-linearization estimate is valid.
Directional scalar consequence of the uniform segment estimate.
After pairing with the segment direction z, the vector estimate becomes the scalar estimate
used in the source integration argument:
inner p z is close to inner p₀ z + t * inner z (B z), uniformly for 0 ≤ t ≤ 1.
A subgradient on a neighborhood of a differentiability point is the gradient.
This is the convex-analysis normalization used in the source proof: once u is differentiable
at x, every supporting slope at x is forced to be ∇u(x).
A subgradient on a neighborhood of a differentiability point is gradient u x.