Almost everywhere differentiability of a convex function #
A proper convex function on a finite-dimensional space is differentiable at almost every point of the interior of its effective domain, the points of differentiability are dense there, and the gradient map is continuous where it is defined.
Main results #
HasGradientAt.hasFDerivAt_toReal,hasGradientAt_of_hasFDerivAt_toReal— the dictionary between∇ffor anEReal-valuedfand Mathlib'sfderivof the real tracefun z => (f z).toReal, valid at interior points ofdom f.exists_lipschitzOnWith_ball— a proper convex function is Lipschitz on a whole ball around any interior point of its effective domain.ae_differentiableAtFn,interior_dom_subset_closure_differentiableAtFn,continuousOn_fderiv_toReal— the almost-everywhere, density and continuity clauses (Theorem 25.5 in [^1]);continuousOn_fderiv_of_convexOnrestates the last for Mathlib'sConvexOn.measure_diff_twoSided_dirDeriv— in a fixed direction the two-sided directional derivative exists almost everywhere, a corollary here rather than the source it classically is.topDualPairing_flip_toDual,mem_subgradient_innerL_iff,conj_innerL_eq_conj_topDualPairing,subgradient_innerL_eq_singleton— the Riesz bridge between the two pairings the library uses on an inner-product space, which is what lets results stated forinnerₗ E, whose subgradients are vectors, speak about gradients, which live inStrongDual ℝ E.normalCone_innerₗ_closedBall— the normal cone to the unit ball at a boundary point is the ray through it. Needs neither finite dimension nor completeness, only Cauchy–Schwarz.
Implementation notes #
Rademacher's theorem, from Mathlib, does the analysis; convexity only supplies local Lipschitz
constants. Convexity gives them on compact subsets of ri (dom f), and
exists_lipschitzOnWith_ball shrinks a closed ball to an open one, so that
DifferentiableWithinAt upgrades to DifferentiableAt. The density clause is stated without any
measure: a non-empty open set has positive Haar measure, so it cannot sit inside a null set.
The classical implication runs the other way — the fixed-direction statement first, by a Fubini argument over lines, then full differentiability by intersecting the coordinate directions. With Rademacher available differentiability comes first, since it supplies the two-sided derivative in every direction at once.
References #
[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §25.
Differentiability through the real trace #
Near an interior point of its effective domain, a proper function is the coercion of its
real trace fun z => (f z).toReal.
A gradient of f is a Fréchet derivative of its real trace.
Conversely, at an interior point of dom f a Fréchet derivative of the real trace is a
gradient of f.
Mathlib's fderiv of the real trace is ∇f.
The gradient of f at a point of differentiability, named.
Differentiability almost everywhere #
A proper convex function is Lipschitz on a whole ball around any interior point of its effective domain. Balls are what Rademacher's theorem needs, because differentiability within an open set is differentiability.
A proper convex function is differentiable at almost every point of the interior of its effective domain.
The points of int (dom f) at which f fails to be differentiable form a null set.
Where f is differentiable, every two-sided directional derivative exists. Both sides are
values of the gradient.
In any fixed direction y the two-sided directional derivative exists at almost every point
of int (dom f). Here this is a consequence of almost-everywhere differentiability, which supplies
the two-sided derivative in every direction at once.
The points of differentiability are dense in the interior of the effective domain. No measure appears in the statement; the proof borrows one.
Continuity of the gradient #
The Riesz bridge at the level of the pairings themselves: pairing x with the vector v
through the inner product is pairing x with the functional ⟪v, ·⟫ through the canonical
pairing of E with its continuous dual. Everything below is this identity under a quantifier.
The Riesz bridge for the conjugate: mem_subgradient_innerL_iff with conj in place of
subgradient. It carries results stated on a general normed space with the pairing
⟨x, y⟩ = y x over to statements about conj (innerₗ E).
The Riesz bridge between the two pairings of an inner-product space with itself and with its
dual: v is a subgradient for innerₗ E exactly when the functional ⟪v, ·⟫ is one for the
canonical pairing with the dual.
In vector form: at a point of differentiability the subdifferential for the inner-product pairing is the single vector representing the gradient.
The Riesz bridge for singletons: a subdifferential that is the single vector v for the
inner-product pairing is the single functional ⟪v, ·⟫ for the canonical pairing with the dual.
Converse, in vector form: a lone subgradient for the inner-product pairing is the gradient.
The gradient mapping is continuous on the set where the function is differentiable. This is
upper semicontinuity of ∂f with both subdifferentials collapsed to singletons.
A finite convex function differentiable on an open convex set is continuously differentiable
there. Mathlib's ConvexOn enters by extension with ⊤ off C, which on the open set C has the
same gradients.
The normal cone to the unit ball #
The normal cone to the unit ball at a boundary point is the ray through that point:
N_B(x) = {λx | λ ≥ 0} for ‖x‖ = 1. It is what turns the optimality condition at a maximiser
over the ball into the eigenvalue condition λx ∈ ∂f(x). Both inclusions are the equality case of
Cauchy–Schwarz, so neither finite-dimensionality nor completeness is needed.