Rockafellar, §25: Differentiability of Convex Functions #
The relation between the subdifferential ∂f and the ordinary gradient ∇f. Theorem 25.1
identifies the two where ∇f exists, Theorems 25.3–25.5 say that is almost everywhere on
int (dom f), Theorem 25.6 reconstructs the whole of ∂f from ∇f, and Theorem 25.7 says that
gradients of convex functions converge whenever the functions do.
All eleven numbered results of §25 are formalized: Theorems 25.1–25.7 and Corollaries 25.1.1,
25.1.2, 25.1.3, 25.5.1. Theorem 25.3 is stated over ℝ rather than Rn 1, the book's I being an
open interval of the real line; the rest is over Rn n with pairing n.
Rockafellar's ∇f(x) is a vector, while the backbone's gradient is a continuous linear
functional. HasGradientVecAt f b x and gradientVec f x are the vector readings, translated by
linFn, which is the Fréchet–Riesz map. Differentiability of an extended-real-valued f is
DifferentiableAtFn: a real-valued function agreeing with f near x and differentiable there,
which is exactly what ∇f(x) presupposes. differentiableAtFn_iff_differentiableAt is the
dictionary to Mathlib's DifferentiableAt of the real trace.
Not all of §25 is finite-dimensional. Theorem 25.1's forward half, both halves of Corollary 25.1.1,
Theorem 25.2's necessity and Theorem 25.4's density clause hold over any normed space. What
genuinely needs ℝⁿ is Theorem 25.1's converse, which runs through Corollary 11.6.1, together with
the continuity and measure-zero clauses of Theorems 25.4 and 25.5.
References #
- R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §25.
∇f(x) as a vector #
Rockafellar's ∇f(x) = b, with b a vector of ℝⁿ: f agrees near x with a
real-valued function whose Fréchet derivative at x is ⟨·, b⟩.
Equations
Instances For
Differentiability in the sense of §25 is the existence of a gradient vector.
∇f(x) as a vector, defined for every x and correct where f is differentiable: the
Riesz representative of Mathlib's derivative of the real trace of f.
Equations
- Rockafellar.gradientVec f x = (InnerProductSpace.toDual ℝ (TdafSurface.Rn n)).symm (fderiv ℝ (fun (z : TdafSurface.Rn n) => (f z).toReal) x)
Instances For
The gradient vector is unique where it exists, and gradientVec computes it.
Where f is differentiable, gradientVec f x is its gradient.
The finite case. Where the book says "let f be a finite convex function", the gradient
is Mathlib's Fréchet derivative of a real-valued function, and this is the translation.
The dictionary to Mathlib. At an interior point of dom f — and by Corollary 25.1.1 there
is nowhere else to look — differentiability in §25's sense is ordinary differentiability of the
real trace z ↦ (f z).toReal.
Theorem 25.1 and its corollaries #
Theorem 25.1, forward half. For a convex f finite at x and differentiable there,
∇f(x) is the unique subgradient of f at x. Nothing in the argument is finite-dimensional,
and the uniqueness half uses neither convexity nor properness.
Theorem 25.1, the displayed inequality: f(z) ≥ f(x) + ⟨∇f(x), z - x⟩ for every z. Like
the forward half it holds over any normed space.
Theorem 25.1, converse half, and this one is genuinely finite-dimensional. If a proper
convex f has a unique subgradient at x then f is differentiable at x. In finite dimensions
a convex set is a neighbourhood of every point whose normal cone is trivial (Corollary 11.6.1),
which is the step Rockafellar passes over.
Rockafellar, Theorem 25.1, in full: for a proper convex function on ℝⁿ, having gradient
b at x and having b as sole subgradient at x are the same thing.
Theorem 25.1 as the book's following sentence states it: ∂f(x) is a single vector exactly
when f is differentiable at x.
Corollary 25.1.1, second half: a convex function finite and differentiable at x is
proper. This holds in any topological vector space.
Corollary 25.1.1, first half: x ∈ int (dom f). It uses neither convexity nor
differentiability, only that f is finite near x, which the definition of ∇f(x) presupposes.
Corollary 25.1.2: for a proper convex f on ℝⁿ, the exposed points of epi f* are the
points (x*, f*(x*)) such that f is differentiable at some x with ∇f(x) = x*. f need not
be closed, as in the book, which replaces f by cl f on the strength of its unproved remark
∇(cl f) = ∇f; that remark needs int (dom (cl f)) = int (dom f) as well as cl f = f on the
interior, and both halves are in the backbone.
Corollary 25.1.3: let C be a non-empty closed convex set and g a positively homogeneous
proper convex function with C = {z | ⟨y, z⟩ ≤ g(y) for all y}. Then z is an exposed point of C
iff g is differentiable at some y with ∇g(y) = z. Non-emptiness and closedness of
supportSet (pairing n) g follow from the other hypotheses and are not assumed.
Theorem 25.2 #
Theorem 25.2, necessity: at a point of differentiability the directional derivative is the
linear function y ↦ ⟨∇f(x), y⟩. General, like Theorem 25.1's forward half.
Theorem 25.2: for a convex f finite at x, differentiability at x is equivalent to
linearity of f'(x; ·). Sufficiency is where ℝⁿ is used, through a cross-polytope estimate that
consumes only the 2n one-sided derivatives along ± bⱼ.
Theorem 25.2, last sentence: differentiability at x already follows from the existence
and finiteness of the n two-sided partial derivatives there.
Theorem 25.3, on the line #
Rockafellar's I is an open interval of ℝ on which f is finite; it is interior (dom f) here.
His f' is defined on D only, while rightDeriv f is defined everywhere and agrees with f' on
D, so the clauses below are the book's, strengthened.
Theorem 25.3, the definition of D: on the line, differentiability at an interior point of
dom f is exactly equality of the two one-sided derivatives.
Theorem 25.3, first assertion: D contains all but countably many points of I.
Rockafellar, Theorem 25.3, the parenthesis: D is dense in I.
Theorem 25.3, second assertion: f' is continuous relative to D — here in the stronger
form that rightDeriv f is continuous at each point of D in the ordinary sense. This is the
clause that wants the book's extension of f to a closed proper convex function on the line.
Theorem 25.3, third assertion: f' is non-decreasing relative to D. Again stronger:
rightDeriv f is monotone on the whole line.
Theorem 25.4 #
Theorem 25.4, first assertion: for proper convex f and fixed y, the two-sided
directional derivative exists at a point of int (dom f) exactly where x ↦ f'(x; y) is
continuous. Rockafellar's y ≠ 0 is not needed — at y = 0 both sides hold.
Theorem 25.4, density — and this clause is general: restricting f to the line through
x in the direction y turns it into Theorem 25.3.
Theorem 25.4, the measure-zero clause. The implication runs the other way here: Rockafellar proves this first, by a Fubini argument over lines, and deduces Theorem 25.5; with Rademacher's theorem available, Theorem 25.5 comes first and this is its consequence.
Theorem 25.5 and its corollary #
Theorem 25.5, density: the set of points where a proper convex function is differentiable
is dense in int (dom f).
Theorem 25.5, measure zero: the complement of D in int (dom f) is null. This is
Rademacher's theorem; convexity contributes only the local Lipschitz constants.
Theorem 25.5, continuity: x ↦ ∇f(x) is continuous on D. This is Corollary 24.5.1 with
both subdifferentials collapsed to singletons by Theorem 25.1.
Corollary 25.5.1: a finite convex function differentiable on an open convex set C is
continuously differentiable on C. The book states this with no proof at all. The proof here
extends g by +∞ off C and applies Theorem 25.5's continuity clause.
Theorem 25.6 #
Rockafellar's S(x): the set of limits of sequences of gradients ∇f(xᵢ) taken at points
of differentiability xᵢ → x. This is gradientLimits in the surface's vector vocabulary.
For x with ∂f(x) ≠ ∅, the recession cone of ∂f(x) is the normal cone to dom f at x.
Rockafellar leaves this as a §23 exercise and says it will be verified inside the proof of Theorem
25.6; it is not — that proof uses only ⊆, and the equality is discharged separately.
Theorem 25.6: for a closed proper convex f whose dom f has non-empty interior,
∂f(x) = cl (conv S(x)) + K(x),
where K(x) is the normal cone to dom f at x and S(x) is gradientLimits f x. The book
declares K(x) empty off dom f, whereas normalCone is total; the two readings agree wherever
both sides are non-empty, and off dom f the left side is empty, forcing cl (conv S(x)) to be
empty too.
Theorem 25.7 #
Theorem 25.7: for C open convex and convex fᵢ, g finite and differentiable on C
with fᵢ → g pointwise on C, one has ∇fᵢ(x) → ∇g(x) for every x ∈ C. For arbitrary
differentiable functions this is false; convexity supplies it through the upper semicontinuity of
∂f under pointwise convergence (Theorem 24.5).
Theorem 25.7, the sentence after it: ∇fᵢ → ∇g uniformly on every closed bounded subset of
C. "Closed and bounded" is IsCompact in ℝⁿ.