The subdifferential reconstructed from the gradient mapping #
For a closed proper convex f whose effective domain has interior,
∂f x = cl (conv (S x)) + N_{dom f}(x) for every x,
where S x is the set of limits of gradients ∇f xᵢ at points of differentiability xᵢ → x.
Every subgradient, at a boundary point of dom f as much as at an interior one, is therefore
assembled out of honest gradients and normal directions.
Main definitions #
gradientLimits f x— the setS x, as a set of vectors: gradients are recorded by their Riesz representatives, so thatS xlives in the same space as∂f xdoes forinnerₗ E.
Main results #
containsNoLine_subgradient—∂f xcontains no line, whendom fhas interior.recessionCone_subgradient_eq_normalCone— the recession cone of∂f xisN_{dom f}(x).exists_mem_interior_dom_of_forall_normalCone— the separation step: a direction making a strictly obtuse angle with every non-zero normal todom fatxreachesint (dom f).exposedPoints_subset_gradientLimits— the heart of the proof: every exposed point of∂f xis a limit of gradients.subgradient_eq_closure_convexHull_gradientLimits_add_normalCone— the reconstruction itself (Theorem 25.6 in [^1]).
Implementation notes #
The recession cone of ∂f x never has to be computed. The classical proof identifies it with
N_{dom f}(x) and uses that three times — to see that ∂f x contains no lines, to place extreme
directions in the normal cone, and to bound ⟨y, y*⟩ for normals y* — but each of those follows
more cheaply from the single inclusion ∂f x + N_{dom f}(x) ⊆ ∂f x of Subgradient/Calculus.lean
together with a "let λ → ∞ in the subgradient inequality" argument. So
recessionCone_subgradient_eq_normalCone is proved on its own and used nowhere below.
References #
[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §25.
The set S x of limits of gradients ∇f xᵢ at points of differentiability xᵢ tending to
x, as a set of vectors: the gradient is an element of StrongDual ℝ E, and what is recorded here
is its Riesz representative, so that S x lives in the same space as ∂f x for innerₗ E.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A gradient at x itself is a limit of gradients, along the constant sequence.
S x ⊆ ∂f x: the graph of ∂f is closed, so a limit of gradients at points tending to x
is a subgradient at x.
A subgradient plus a multiple of a normal direction is a subgradient, packaged for the
innerₗ pairing.
The subgradient inequality at v + a • w, as a bound between real numbers. Both f z and
f x are finite — the first because z ∈ dom f, the second because a subgradient exists at x —
so the EReal inequality is a real one, and the pairing splits by bilinearity.
The subdifferential contains no line once dom f has interior. If v + t w ∈ ∂f x for
every real t, the subgradient inequality forces ⟨z - x, w⟩ = 0 on all of dom f, and a set
with interior lies in no hyperplane.
A direction of recession of ∂f x is normal to dom f at x. Letting λ → ∞ in the
subgradient inequality for v + λ w forces ⟨z - x, w⟩ ≤ 0 on dom f.
Wherever ∂f x is non-empty, its recession cone is the normal cone to dom f at x. The
reconstruction below uses only the inclusion recessionCone_subgradient_subset_normalCone, so this
equality is discharged here on its own: the other inclusion is ∂f x + N_{dom f}(x) ⊆ ∂f x read at
a single normal direction.
The separation step. If every non-zero vector normal to dom f at x makes a strictly
obtuse angle with y, then the half-line from x in the direction y reaches int (dom f).
Contrapositive plus geometric_hahn_banach_open: if the half-line missed the open convex set
int (dom f), the separating functional would be a non-zero normal making a non-obtuse angle with
y. Proper separation is not needed.
Points of differentiability approaching x from the direction y. If the ray from x in
the unit direction y enters int (dom f), density of the points of differentiability supplies
points arbitrarily close to it. The tolerance has to be ε² at distance ε, not ε:
it is the direction of approach that must converge to y.
The substantive step: an exposed point of ∂f x is a limit of gradients.
If the functional exposing x* is zero the subdifferential is the single point x*, and a lone
subgradient makes f differentiable at x itself. Otherwise its Riesz representative y,
normalised, makes a strictly obtuse angle with every non-zero normal to dom f at x, so the ray
x + α y enters int (dom f); density supplies points of differentiability approaching x in the
direction y, and the boundary convergence theorem collapses their subdifferentials onto the face
of ∂f x exposed by y, which is {x*}.
For a closed proper convex function whose effective domain has interior, the subdifferential at any point is reconstructed from the gradient mapping,
∂f x = cl (conv S(x)) + N_{dom f}(x),
where S(x) is the set of limits of gradients at points of differentiability tending to x.
The inclusion ⊇ is closedness and convexity of ∂f x together with
∂f x + N_{dom f}(x) ⊆ ∂f x. The inclusion ⊆ is the extreme-point representation of a line-free
closed convex set — ∂f x contains no lines, so it is the convex hull of its extreme points and
extreme directions — with Straszewicz's theorem carrying the extreme points into the closure of
the exposed ones, which exposedPoints_subset_gradientLimits places in S(x), and
recessionCone_subgradient_subset_normalCone carrying the extreme directions into the normal
cone.