Convex functions of Legendre type #
A closed proper convex function is of Legendre type when it is essentially smooth and strictly
convex on the interior C of its effective domain — equivalently, when ∂f is a one-to-one
mapping. The property is self-dual: f is of Legendre type exactly when f* is, and then ∇f is
a bijection of C onto C* = int (dom f*), continuous in both directions, with ∇f* = (∇f)⁻¹.
For an essentially smooth function the domain D of the Legendre conjugate is dom ∂f*, and so is
squeezed between ri (dom f*) and dom f*. In general D is not convex, which is why the squeeze
cannot be improved to an equality.
Main definitions #
gradientRange f— the setD = ∇f(C), as a set of vectors.LegendreType f—fis essentially smooth and strictly convex onint (dom f).
Main results #
hasGradientAt_toDual_iff_mem_subgradient— for an essentially smoothf, being the gradient atxand being a subgradient atxsay the same thing. Everything else here is that equivalence combined with the inversion∂f* = (∂f)⁻¹.gradientRange_eq_domSubgradient_conj,relint_dom_conj_subset_gradientRange,gradientRange_subset_dom_conj—D = dom ∂f*, thereforeri (dom f*) ⊆ D ⊆ dom f*.legendreType_conj_iff,bijOn_gradient_of_legendreType,continuousOn_gradient_interior_dom— the Legendre duality (Theorem 26.5 in [^1]).bijOn_gradient_univ_iff,conj_finite_of_bijOn_gradient_univ— for a finite differentiable convex function,∇fis a bijection ofEonto itself exactly whenfis strictly convex withdom f* = E, and thenf*is a function of the same kind.
Implementation notes #
legendreDom f lives in StrongDual ℝ E, but it has to be compared with dom ∂f*, whose elements
are vectors for the self-pairing innerₗ E. gradientRange is legendreDom carried back across
the Riesz isometry, so that the comparison is an equality of sets in E.
References #
[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §26.
The range of the gradient mapping, in vector form #
The domain D = ∇f(C) of the Legendre conjugate, as a set of vectors: the preimage of
legendreDom f under the Riesz isometry.
Equations
- Tdaf.ConvexAnalysis.gradientRange f = {v : E | ∃ (x : E), Tdaf.ConvexAnalysis.HasGradientAt f ((InnerProductSpace.toDual ℝ E) v) x}
Instances For
Mathlib's gradient of the real trace is ∇f.
At a point of differentiability, gradient (fun w => (f w).toReal) really is a gradient.
The domain of the Legendre conjugate #
For an essentially smooth function, gradients and subgradients coincide. On the interior of the effective domain a lone subgradient is the gradient; off it, both sides are impossible.
For an essentially smooth closed proper convex function the domain D of the Legendre
conjugate is exactly dom ∂f*, the set where f* has a subgradient.
ri (dom f*) ⊆ D: a closed proper convex function has a subgradient at every point of the
relative interior of its effective domain, applied to f*.
D ⊆ dom f*: a point carrying a subgradient of f* is a point where f* is finite.
The Legendre conjugate g — which is f* restricted to D — is strictly convex on every
convex subset of D.
Functions of Legendre type #
A convex function of Legendre type: essentially smooth, and strictly convex on the interior of
its effective domain. Classically the property belongs to the pair (C, f), C = int (dom f).
Equations
Instances For
A closed proper convex function is of Legendre type exactly when ∂f is a one-to-one
mapping: at most one subgradient at each point, and no subgradient shared by two points.
Being of Legendre type is self-dual: f* is of Legendre type exactly when f is. Both sides
become single-valuedness and injectivity of a subdifferential, and inverting the subdifferential
swaps those two conditions.
∇f* = (∇f)⁻¹: v is the gradient of f at x exactly when x is that of f* at v.
∇f maps C = int (dom f) onto C* = int (dom f*).
Two points with the same gradient are equal, when f is of Legendre type: both are gradients
of f* at the common value, and a gradient is unique.
∇f is a one-to-one mapping of C onto C*.
∇f* undoes ∇f on C.
∇f undoes ∇f* on C*.
Continuity of the gradient mapping #
∇f is continuous where f is differentiable, with the gradient read as a vector.
For an essentially smooth f, ∇f is continuous on int (dom f). Applied to f and to f*,
this gives continuity of ∇f and of its inverse ∇f*.
Finite differentiable convex functions #
A convex function that is finite and differentiable everywhere is essentially smooth: condition
(c) is vacuous, because every point lies in interior (dom f) = E.
A proper convex function that is finite everywhere is closed.
For a convex function that is finite and differentiable everywhere, ∇f maps E one-to-one
onto E exactly when f is strictly convex and dom f* is all of E. The second condition is
co-finiteness; the recession function does not appear here, so the equation is stated directly.
When ∇f is a one-to-one mapping of E onto itself, f* is again a finite, differentiable,
strictly convex function whose own conjugate domain is everything. The hypotheses are therefore
self-dual.