Gradients and the subdifferential #
Where a convex function is differentiable its gradient is its only subgradient, and the directional
derivative is the corresponding linear function. Conversely, for a convex function finite at x,
differentiability at x is equivalent to linearity of f'(x; ·), and in finite dimensions the
two-sided derivatives along the vectors of a basis already suffice.
Dually, a point of epi f* is exposed exactly when it is (y, f* y) for a y that is the only
subgradient of f somewhere, and the same holds for the set cut out by a positively homogeneous
function. Both are phrased in terms of unique subgradients rather than of differentiability: the
converse passage needs x interior to dom f and is in Subgradient/Uniqueness.lean.
Main results #
subgradient_eq_singleton_of_dirDeriv_eq,clFn_dirDeriv_eq_of_subgradient_eq_singleton— iff'(x; ·)is⟨·, y₀⟩then∂f x = {y₀}, and conversely a single-valued∂f xmakescl f'(x; ·)linear.le_hasFDerivAt,subgradient_eq_singleton_of_hasFDerivAt— the gradient inequalityf z ≥ f x + ⟨z - x, ∇f x⟩, and∂f x = {∇f x}(Theorem 25.1 in [^1]). The uniqueness half alone,eq_of_mem_subgradient_of_hasFDerivAt, needs no convexity.differentiableAtFn_iff_exists_dirDeriv_eq,differentiableAtFn_of_forall_basis_dirDeriv_eq— differentiability is linearity off'(x; ·), already along a basis (Theorem 25.2 in [^1]).mem_exposedPoints_epi_conj_iff,mem_exposedPoints_supportSet_iff— exposed points as unique subgradients.HasGradientAt,DifferentiableAtFn—∇f x = f'for anEReal-valuedf, with the results above repackaged as.le,.subgradient_eq,.dirDeriv_eq,.mem_interior_dom,.properand.unique. This is the interface the Legendre theory uses.
Implementation notes #
Differentiability of an EReal-valued function is carried by a local real representative:
HasFDerivAt needs a normed target, so a convex f : E → EReal is differentiable at x when some
real g has f =ᶠ[𝓝 x] fun z => (g z : EReal) and HasFDerivAt g f' x. This forces
x ∈ int (dom f), the standing assumption that f x is finite. Restricting to f : E → ℝ instead
would lose the Legendre theory, where the interesting functions are +∞ outside an open set.
The directional-derivative statements hold over an arbitrary pairing B, with uniqueness needing
B separating in its second variable. In place of [FiniteDimensional ℝ E] the exposed point
results assume [IsCompatiblePairing B.flip] — every continuous linear functional on F is
⟨x, ·⟩ — which holds for finite-dimensional E paired with StrongDual ℝ E.
References #
[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §25.
The algebraic core: a linear directional derivative #
Algebraically: if the directional derivative f'(x; ·) is the linear function ⟨·, y₀⟩, then
y₀ is the unique subgradient of f at x. This is the description of ∂f x by
⟨·, y⟩ ≤ f'(x; ·) plus the observation that ⟨v, y⟩ ≤ ⟨v, y₀⟩ for every v, -v included,
forces ⟨·, y⟩ = ⟨·, y₀⟩; the pairing must therefore separate the points of F.
The converse at the level of closures: if ∂f x is a single point y₀, then cl f'(x; ·) is
the linear function ⟨·, y₀⟩. It is cl f'(x; ·) = δ*(· | ∂f x), the support function of a
singleton being linear.
Rays and difference quotients #
The ray t ↦ x + t • v tends to x as t ↓ 0.
The difference quotient along a ray converges to the derivative in that direction. This is the only piece of calculus the section uses.
Local finiteness and properness #
A function that agrees with a real-valued function near x has x in the interior of its
effective domain. Neither convexity nor differentiability plays any role — only local
finiteness.
A convex function that is finite near a point is proper. Unlike the general statement that a
convex function taking −∞ takes it throughout the relative interior of its domain, this holds in
any topological vector space: if f u = ⊥ then f is ⊥ on the half-open segment [u, x),
whose points approach x, where f is finite.
The gradient is the unique subgradient #
The gradient inequality: a convex function lies above its tangent affine function at every point of differentiability.
Uniqueness: any subgradient at a point of differentiability is the derivative. Neither convexity nor properness is used — only the limit of the difference quotient along the two opposite rays.
At a point where a convex function is differentiable, the gradient is the unique subgradient.
Necessity: at a point of differentiability the directional derivative is the linear
function v ↦ ⟨v, ∇f x⟩. Both halves come from the defining infimum: the lower bound is the
gradient inequality at x + a • v, the upper bound the limit a ↓ 0, extracted through
EReal.lt_iff_exists_real_btwn so that no EReal division has to be computed.
f has gradient f' at x: near x, f agrees with a real-valued function that is
Fréchet differentiable at x with derivative f'. This is ∇f x = f'. An EReal-valued function
cannot satisfy HasFDerivAt directly — that needs a normed target — and the local real
representative carries exactly what the classical definition presupposes: f finite near x.
Equations
- Tdaf.ConvexAnalysis.HasGradientAt f f' x = ∃ (g : E → ℝ), (f =ᶠ[nhds x] fun (z : E) => ↑(g z)) ∧ HasFDerivAt g f' x
Instances For
f is differentiable at x: it has a gradient there.
Equations
- Tdaf.ConvexAnalysis.DifferentiableAtFn f x = ∃ (f' : StrongDual ℝ E), Tdaf.ConvexAnalysis.HasGradientAt f f' x
Instances For
Packaged: a gradient at x puts x in the interior of dom f.
Packaged: a convex function with a gradient somewhere is proper.
The gradient inequality, packaged.
Packaged: the gradient is the only subgradient.
Packaged: f'(x; v) = ⟨v, ∇f x⟩ at a point of differentiability.
The gradient is unique where it exists. This is the
uniqueness of HasFDerivAt for the local real representative, and it needs no convexity.
From directional derivatives back to the gradient #
The two-sided one-dimensional estimate behind sufficiency. If the directional derivatives
of f at x along v and -v are c and -c, then for every η > 0 there is a step a₀ > 0
with
f (x + t • v) ≤ f x + t * c + |t| * η whenever |t| ≤ a₀,
for t of either sign. On the negative side the one-sided estimate is applied in the direction
-v; the linear term survives unchanged because (-t) * (-c) = t * c, while the error term picks
up |t| = -t.
Sufficiency, quantitatively: two-sided directional derivatives along a basis already force the tangent affine estimate
f z ≤ f x + ⟨z - x, y₀⟩ + ε ‖z - x‖
on a ball whose radius depends only on ε.
Finite-dimensionality enters through a cross-polytope decomposition rather than through
compactness of the unit sphere, which keeps the argument quantitative. Writing z - x = ∑ ξ j • b j
and S = ∑ |ξ j|, the point z is the convex combination with weights |ξ j| / S of the points
x + (S * sign (ξ j)) • b j, each at distance S from x along a basis direction, where the
one-sided estimate applies. The linear terms recombine into ⟨z - x, y₀⟩ exactly and the error is
S * η, at most ε ‖z - x‖ once η is scaled by the constant relating ∑ |ξ j| to ‖z - x‖.
The estimate of exists_le_of_forall_basis_dirDeriv_eq recovers f'(x; ·) in every
direction, not only along the basis: it bounds f'(x; v) above by ⟨v, y₀⟩, and the general
inequality -f'(x; -v) ≤ f'(x; v) supplies the matching lower bound. This turns n two-sided
partial derivatives into linearity of f'(x; ·) without a detour that would need f'(x; ·) to be
proper first.
Sufficiency, from two-sided derivatives along a basis: f is Fréchet differentiable at
x, with gradient the functional y₀ whose values along the basis are the given
one-sided derivatives. The two-sided estimate f x + ⟨z - x, y₀⟩ ≤ f z ≤ f x + ⟨z - x, y₀⟩ + ε ‖z - x‖ does all three jobs at once: it makes f finite near x, so that the local real
representative exists, and exhibits the little-o estimate defining HasFDerivAt.
Sufficiency: if the directional derivative f'(x; ·) is the linear function ⟨·, y₀⟩,
then f is differentiable at x with ∇f x = y₀. This is the previous theorem read at any basis;
the hypothesis in every direction is more than the proof consumes.
In full: for a convex function finite at x, differentiability at x is equivalent to
linearity of f'(x; ·). Necessity is HasGradientAt.dirDeriv_eq and sufficiency is
hasGradientAt_of_dirDeriv_eq.
It is already enough that the n two-sided partial derivatives exist and are finite. Here
"the n partial derivatives" is the pair of one-sided derivatives along the vectors of a basis,
and "two-sided and finite" is the requirement that they be the negatives of each other and real.
The gradient is then b.constr of those numbers.
Exposed points of a half-cylinder #
The exposed points of a half-cylinder C ×ˢ [0, ∞) are the points (z, 0) with z an
exposed point of C. A functional exposing a point of the cylinder must be strictly decreasing
in the vertical direction, since otherwise the whole vertical ray attains the maximum; that forces
the height to be 0 and reduces the functional to one on C. The cylinder is the epigraph of an
indicator function, so this is how a statement about epi f* becomes one about a convex set.
Exposed points of the epigraph of a conjugate #
A subgradient pins down the value: if y ∈ ∂f x and f* y = μ is finite, then
f x = ⟨x, y⟩ - μ. This is Fenchel's equality solved for f x, and in particular f x is
finite.
In subgradient form: (y, μ) is an exposed point of epi f* exactly when μ = f* y and y
is the only subgradient of f at some point x.
Geometrically, a supporting hyperplane to epi f* touching it in a single point is necessarily
non-vertical, hence the graph of an affine function ⟨x, ·⟩ - α; supporting epi f* at (y, μ)
says x ∈ ∂f*(y), i.e. y ∈ ∂f x, and touching nowhere else says ∂f x is no larger than {y}.
Only the forward direction uses closedness, through ∂f* = (∂f)⁻¹.
Exposed points of a set cut out by a positively homogeneous function #
The exposed points of a set are the values of the subdifferential of any positively
homogeneous function that cuts it out. If g is closed proper convex and positively
homogeneous and C = {x | ⟨x, y⟩ ≤ g y for all y} — for instance g the support function of
C — then z is an exposed point of C exactly when z is the only subgradient of g at some
y. The conjugate of g is the indicator of C, so epi g* is the half-cylinder C ×ˢ [0, ∞)
and this is the previous result read at height 0.