Rockafellar, §26: The Legendre Transformation #
The classical Legendre transformation, and the exact sense in which it is the conjugacy correspondence restricted to the functions whose subdifferential is a genuine one-to-one mapping.
All eleven numbered results of §26 are formalized over Rn n = ℝⁿ: Theorems 26.1, 26.3, 26.4,
26.5, 26.6, Lemmas 26.2 and 26.7, and Corollaries 26.3.1, 26.3.2, 26.3.3, 26.4.1, together with all
three of the section's counterexamples, transcribed as Lean definitions.
SingleValued, inverseMap and OneToOne are the book's vocabulary for multivalued mappings
(p. 251), and legendreDomain f is Rockafellar's D, the image of C = int (dom f) under the
gradient mapping. LegendreType is the backbone's, and says exactly what the book's "the pair
(C, f) is a convex function of Legendre type" says for C = int (dom f). Essential smoothness is
carried in two equivalent forms — EssentiallySmoothBook, with the book's condition (c), and
EssentiallySmoothDir, with its directional form (c′), the equivalence being Lemma 26.2 — because
a limit-of-gradients argument produces (c) while a user with a concrete f can check (c′). The
backbone's EssentiallySmooth quantifies (c) over points outside C rather than over boundary
points of C; the two agree, and essentiallySmooth_iff_book proves it.
Three of the book's hypotheses are stronger than its own proofs need. Theorem 26.5 says "closed
convex function" where its proof needs "closed proper convex", so theorem_26_5 carries
Proper f; nothing is lost, since an improper closed convex function is +∞ everywhere or −∞ on
cl (dom f) and so is differentiable on no non-empty interior. Theorem 26.4's single-valuedness
and its formula g = f* follow from convexity alone, so theorem_26_4_wellDefined and
theorem_26_4_eq carry only ConvexFn f. Corollary 26.3.3's "A maps ℝⁿ onto ℝᵐ" is used
only through injectivity of A* — the book's own proof says so parenthetically.
There is deliberately no involution lemma for the Legendre transformation. The book is explicit
(p. 258) that the Legendre conjugate of the Legendre conjugate need not be the original function;
Theorem 26.5 says exactly when it is, and not_convex_legendreDomain_halfPlaneFn is why its
hypothesis cannot be dropped.
References #
- R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §26.
Multivalued mappings #
§26 (p. 251). A multivalued mapping ρ is single-valued when ρ x has at most one
element for each x. Its effective domain need not be all of ℝⁿ.
Equations
- Rockafellar.SingleValued ρ = ∀ (x : TdafSurface.Rn n), (ρ x).Subsingleton
Instances For
Rockafellar, §26 (p. 251). The inverse of a multivalued mapping,
ρ⁻¹ x* = {x | x* ∈ ρ x}.
Equations
- Rockafellar.inverseMap ρ y = {x : TdafSurface.Rn n | y ∈ ρ x}
Instances For
Rockafellar, §26 (p. 251). A multivalued mapping is one-to-one when both it and its
inverse are single-valued — equivalently, when graph ρ contains neither two different pairs with
the same first component nor two with the same second component.
Equations
Instances For
Single-valuedness of ρ⁻¹ is the statement that ρ takes distinct points to disjoint sets,
which is the form the backbone's injectivity theorems are stated in.
The bridge between the book's "one-to-one" and the backbone's injectivity.
Essential smoothness #
A proper convex function f is essentially smooth (p. 251) when, for C = int (dom f):
- (a)
Cis not empty; - (b)
fis differentiable throughoutC; - (c)
|∇f xᵢ| → +∞wheneverx₁, x₂, …is a sequence inCconverging to a boundary point ofC.
Rockafellar, §26 (p. 251), verbatim: conditions (a), (b) and (c) with (c) quantified over
boundary points of C = int (dom f), as the book quantifies it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The book's condition (c) and the backbone's are the same condition. C = int (dom f) is
open, so its frontier is cl C \ C: a boundary point of C is not in C, and conversely a point
outside C that a sequence in C converges to lies on the boundary.
Theorem 26.1 #
Rockafellar, Theorem 26.1. Let f be a closed proper convex function. Then ∂f is a
single-valued mapping if and only if f is essentially smooth.
Rockafellar, Theorem 26.1, the "in this case" clause, first half: ∂f x consists of the
vector ∇f x alone when x ∈ int (dom f).
Rockafellar, Theorem 26.1, the "in this case" clause, second half: ∂f x = ∅ when
x ∉ int (dom f). This is the substantive half — it is what makes ∂f an ordinary function on
int (dom f) and nothing anywhere else.
Rockafellar, Theorem 26.1, both halves of the "in this case" clause as one equation:
dom ∂f = int (dom f) for an essentially smooth closed proper convex function.
Lemma 26.2 #
Rockafellar, Lemma 26.2, conditions (a), (b), (c′): the definition of essential smoothness with condition (c) replaced by
(c') f'(x + λ(a − x); a − x) ↓ −∞ as λ ↓ 0, for any a ∈ C and any boundary point x of C.
The ↓ of the book records that the map is nondecreasing in λ, which holds for every convex f;
the content of (c′) is the value of the limit, so only the limit appears here.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Rockafellar, Lemma 26.2, at a single point: assuming (a) and (b), condition (c) at x and
condition (c′) at x along the segment from any a ∈ C say the same thing — namely that f has
no subgradient at x.
Rockafellar, Lemma 26.2. For a closed proper convex function, condition (c) may be replaced by condition (c′): the two definitions of essential smoothness agree.
Essential strict convexity #
A real-valued function is strictly convex on C (p. 253) when the convexity inequality between
two different points of C is strict, and a proper convex function on ℝⁿ is essentially
strictly convex when it is strictly convex on every convex subset of dom ∂f. Both are the
backbone's StrictConvexOnFn and EssentiallyStrictlyConvex, whose definitions are literally the
book's. Rockafellar's two warnings about the definition are the counterexamples below.
Coordinates on ℝ² #
The section's three counterexamples all live on ℝ²; these are the coordinate facts they need.
The counterexample of p. 253 #
Rockafellar's first warning: a closed proper convex function which is essentially strictly convex
need not be strictly convex on the whole of dom f.
§26 (p. 253), the first counterexample:
f(ξ₁, ξ₂) = ξ₂²/2ξ₁ − 2ξ₂^(1/2) if ξ₁ > 0, ξ₂ ≥ 0
= 0 if ξ₁ = 0 = ξ₂
= +∞ otherwise.
The two branches are one formula: at the origin the real expression reads 0/0 − 2√0, which is 0
in Lean, matching the book's second clause. Rockafellar's claim is that this f is essentially
strictly convex — indeed essentially smooth — while not being strictly convex on dom f,
because it vanishes along the whole non-negative ξ₁-axis. Only the second half is formalized, as
essStrictlyConvexFn_not_strictConvexOn_dom.
Equations
Instances For
The p. 253 example vanishes along the whole non-negative ξ₁-axis, which is the book's
observation.
The non-negative ξ₁-axis lies in the effective domain of the p. 253 example.
Rockafellar, §26 (p. 253). The example is not strictly convex on dom f: it is identically
zero along the non-negative ξ₁-axis, which is a convex subset of dom f. This is what separates
essential strict convexity from strict convexity on the effective domain.
The counterexample of p. 254 #
Rockafellar's second warning: a closed proper convex function may be strictly convex on
ri (dom f) and still fail to be essentially strictly convex, because dom ∂f can be strictly
larger than ri (dom f) and can contain a convex set on which f is constant.
§26 (p. 254), the second counterexample:
f(ξ₁, ξ₂) = ξ₂²/2ξ₁ + ξ₂² if ξ₁ > 0, ξ₂ ≥ 0
= 0 if ξ₁ = 0 = ξ₂
= +∞ otherwise.
Encoded exactly as essStrictlyConvexFn is. Rockafellar's claim is that ri (dom f) is the open
positive quadrant, on which f is strictly convex, while dom ∂f also contains the whole
non-negative ξ₁-axis, on which f is constant — so f is not essentially strictly convex.
Both halves are proved below.
Equations
Instances For
The p. 254 example is non-negative everywhere, which is what makes 0 a subgradient at every
point where it vanishes.
The non-negative ξ₁-axis of ℝ².
Instances For
The non-negative ξ₁-axis is convex — which is what makes it admissible in Rockafellar's
definition of essential strict convexity.
The p. 254 example vanishes on the non-negative ξ₁-axis.
The whole non-negative ξ₁-axis lies in dom ∂f for the p. 254 example: the function is
non-negative and vanishes there, so 0 is a subgradient at each of its points. This is exactly
Rockafellar's observation that dom ∂f is bigger than ri (dom f) here.
The p. 254 example vanishes at (t, 0) for t ≥ 0.
Rockafellar, §26 (p. 254). The example is not essentially strictly convex: the non-negative
ξ₁-axis is a convex subset of dom ∂f on which the function is constant.
The p. 254 example is strictly convex on ri (dom f) #
The other half of Rockafellar's claim, and what makes the example separate the two conditions.
ri (dom f) is the open positive quadrant, and strict convexity there is the weighted
Cauchy–Schwarz inequality (au + bv)²/(as + bt) ≤ au²/s + bv²/t together with
(au + bv)² ≤ au² + bv², one of which is strict at any two distinct points of the quadrant.
The open positive quadrant of ℝ², which is ri (dom f) for the p. 254 example.
Instances For
ri (dom f) is the open positive quadrant for the p. 254 example. The domain has
non-empty interior, so ri collapses to interior, and the interior is the quadrant because a
domain point with ξ₂ = 0 has points with ξ₂ < 0 arbitrarily close to it.
§26 (p. 254), the positive half: the example is strictly convex on ri (dom f), the open
positive quadrant. With strictOnRelintFn_not_essentiallyStrictlyConvex this is the whole point of
the example. Neither summand of ξ₂²/2ξ₁ + ξ₂² is strictly convex on the quadrant — the first is
positively homogeneous, hence affine along every ray from the origin, and the second is constant in
ξ₁ — so no sum rule applies; what makes the sum strict is that their directions of affineness are
disjoint.
Theorem 26.3 #
Rockafellar, Theorem 26.3. A closed proper convex function is essentially strictly convex if and only if its conjugate is essentially smooth.
Rockafellar, Theorem 26.3, read at f*: the conjugate of a closed proper convex function is
essentially strictly convex exactly when the function itself is essentially smooth. This is the
direction Corollaries 26.3.2 and 26.3.3 use.
Corollary 26.3.1 #
Rockafellar, Corollary 26.3.1. Let f be a closed proper convex function. Then ∂f is a
one-to-one mapping if and only if f is strictly convex on int (dom f) and essentially smooth.
Corollaries 26.3.2 and 26.3.3: preservation of essential smoothness #
Rockafellar, Corollary 26.3.2. Let f₁ and f₂ be closed proper convex functions on ℝⁿ
such that f₁ is essentially smooth and ri (dom f₁*) ∩ ri (dom f₂*) ≠ ∅. Then f₁ □ f₂ is
essentially smooth.
Rockafellar, Corollary 26.3.3. Let f be a closed proper convex function on ℝⁿ which is
essentially smooth, and let A be a linear transformation from ℝⁿ onto ℝᵐ. If there exists a
y* ∈ ℝᵐ such that A* y* ∈ ri (dom f*), then the convex function Af on ℝᵐ is essentially
smooth.
A* is LinearMap.adjoint A; the surjectivity of A is used only to make A* injective, which is
what the argument consumes.
The Legendre conjugate #
Rockafellar, p. 256. For a differentiable real-valued f on an open set C ⊆ ℝⁿ, the Legendre
conjugate of (C, f) is the pair (D, g) where D = ∇f(C) and
g(x*) = ⟨(∇f)⁻¹(x*), x*⟩ − f((∇f)⁻¹(x*)).
∇f need not be one-to-one for g to be well defined; it suffices that ⟨x, x*⟩ − f(x) be the
same for every x with ∇f x = x*, which is Theorem 26.4's first clause.
Rockafellar, §26 (p. 256). Rockafellar's D: the image of C = int (dom f) under the
gradient mapping.
Equations
- Rockafellar.legendreDomain f = (gradient fun (w : TdafSurface.Rn n) => (f w).toReal) '' interior (Tdaf.ConvexAnalysis.dom f)
Instances For
The bridge to the backbone's gradientRange, valid as soon as condition (b) holds:
{v | ∃ x, ∇f x = v} and "the image of C under ∇f" are the same set, because every gradient is
attained at an interior point of dom f (Corollary 25.1.1) and, on C, Mathlib's gradient of the
real trace is Rockafellar's ∇f.
Theorem 26.4 #
Rockafellar, Theorem 26.4, first clause: the Legendre conjugate (D, g) of (C, f) is
well-defined. Whatever x is chosen in (∇f)⁻¹(x*), the value ⟨x, x*⟩ − f(x) is the same.
Only convexity is needed. The book states the theorem for a closed proper convex f with
non-empty C = int (dom f) on which f is differentiable; the well-definedness is a consequence of
Theorem 23.5 at the two points separately and holds wherever two gradients happen to agree.
Rockafellar, Theorem 26.4, second and third clauses: D ⊆ dom f*, and g is the
restriction of f* to D — at a point x* of D the defining formula returns f*(x*).
Rockafellar, Theorem 26.4: D is a subset of dom f*.
Corollary 26.4.1 #
Rockafellar, Corollary 26.4.1, first clause: for an essentially smooth closed proper convex
f, the domain D of the Legendre conjugate is {x* | ∂f*(x*) ≠ ∅}.
Rockafellar, Corollary 26.4.1: ri (dom f*) ⊆ D, so D is "almost convex".
Rockafellar, Corollary 26.4.1: D ⊆ dom f*, the other half of the squeeze.
Rockafellar, Corollary 26.4.1: g is the restriction of f* to D.
Rockafellar, Corollary 26.4.1, last clause: g is strictly convex on every convex subset
of D. Since g = f* on D (Theorem 26.4), this is the essential strict convexity of f*, which
Theorem 26.3 supplies from the essential smoothness of f.
The counterexample of p. 257: the parabola #
Rockafellar, p. 257: if f is a differentiable convex function on a non-empty open convex set C
failing condition (c), the domain D of the Legendre conjugate need not be almost convex. The
witness is ξ₁²/4ξ₂ on the open upper half-plane, whose D is the parabola ξ₂* = −(ξ₁*)².
Without condition (c) the squeeze ri (dom f*) ⊆ D ⊆ dom f* of Corollary 26.4.1 fails, and D
need not even be convex.
Rockafellar, §26 (p. 257). The parabola P = {(ξ₁*, ξ₂*) | ξ₂* = −(ξ₁*)²}.
Instances For
Rockafellar, §26 (p. 257). f(ξ₁, ξ₂) = ξ₁²/4ξ₂ on the open upper half-plane, extended by
+∞, so that C = int (dom f) is exactly the open upper half-plane.
Instances For
C = int (dom f) is the open upper half-plane, as the book takes it to be.
The p. 257 example is convex: "quadratic over linear" is jointly convex, and the identity
that says so is A − B = ab(ξ₁ η₂ − η₁ ξ₂)² / 4ξ₂η₂(aξ₂ + bη₂).
The subdifferential of ξ₁²/4ξ₂ in coordinates. Both directions come from the same
completed square: ξ₁²/4ξ₂ − u₀ξ₁ − u₁ξ₂ = (ξ₁ − 2u₀ξ₂)²/4ξ₂ − ξ₂(u₀² + u₁), whose infimum over
the ray ξ = (2su₀, s) is −s(u₀² + u₁). Testing at s = ξ₂, s = ξ₂ + 1 and s = ξ₂/2 forces
both u₀² + u₁ = 0 and the completed square to vanish, with no case analysis.
On the open upper half-plane the subdifferential of the p. 257 example is the single vector
(ξ₁/2ξ₂, −ξ₁²/4ξ₂²), which lies on the parabola.
The p. 257 example is differentiable throughout C, its gradient at x being the single
subgradient there (Theorem 25.1 backwards).
Rockafellar, §26 (p. 257). The image D of C under ∇f is exactly the parabola: as
x runs over the open upper half-plane, ξ₁/2ξ₂ runs over all of ℝ, and the second coordinate
of the gradient is forced to be minus its square.
Rockafellar, §26 (p. 257). D is the parabola, in the book's own legendreDomain.
Rockafellar, §26 (p. 257), the point of the example. For a differentiable convex function on
a non-empty open convex set that fails condition (c), the domain D of the Legendre conjugate need
not be convex — let alone "almost convex" in the sense of Corollary 26.4.1.
Rockafellar, §26 (p. 257), last sentence: "Condition (c) fails for f at the origin."
Along the sequence (0, 1/(i+1)), which lies in C and converges to the origin, the gradient is
identically 0; so its norm does not tend to +∞ and the p. 257 example is not essentially
smooth. This is why Corollary 26.4.1 does not apply to it, and hence why
not_convex_legendreDomain_halfPlaneFn is not a contradiction.
Functions of Legendre type #
A pair (C, f) with C open convex and f strictly convex on C satisfying (a), (b) and (c) is
a convex function of Legendre type (p. 258). Since C = int (dom f) is determined by f, this
is the backbone's LegendreType f, which by Corollary 26.3.1 holds exactly when ∂f is
one-to-one.
Rockafellar, p. 258, the characterisation the book states immediately after the definition:
a closed proper convex function f has ∂f one-to-one if and only if the restriction of f to
C = int (dom f) is a convex function of Legendre type.
Theorem 26.5 #
Rockafellar, Theorem 26.5, first assertion. Let f be a closed convex function, and let
C = int (dom f), C* = int (dom f*). Then (C, f) is a convex function of Legendre type if and
only if (C*, f*) is.
Rockafellar, Theorem 26.5: when f is of Legendre type, (C*, f*) is the Legendre
conjugate of (C, f) — the domain half, D = C*.
Rockafellar, Theorem 26.5: the value half of "(C*, f*) is the Legendre conjugate of
(C, f)" — on C the defining formula of the Legendre conjugate returns f*.
Rockafellar, Theorem 26.5: (C, f) is in turn the Legendre conjugate of (C*, f*) — the
domain half. Note the hypothesis: this is the involutivity of the Legendre transformation, and it
holds only within the Legendre-type class. See the module docstring.
Rockafellar, Theorem 26.5: (C, f) is in turn the Legendre conjugate of (C*, f*) — the
value half. Again only within the Legendre-type class.
Rockafellar, Theorem 26.5: the gradient mapping ∇f is one-to-one from the open convex set
C onto the open convex set C*.
Rockafellar, Theorem 26.5: ∇f is continuous on C.
Rockafellar, Theorem 26.5: ∇f is continuous in both directions, the second half being
the continuity of ∇f* on C*.
Rockafellar, Theorem 26.5: ∇f* = (∇f)⁻¹, one composite.
Rockafellar, Theorem 26.5: ∇f* = (∇f)⁻¹, the other composite.
Theorem 26.6 #
Rockafellar, Theorem 26.6. Let f be a (finite) differentiable convex function on ℝⁿ. In
order that ∇f be a one-to-one mapping from ℝⁿ onto itself, it is necessary and sufficient that
f be strictly convex and co-finite.
Rockafellar, Theorem 26.6, the concluding clauses: when ∇f is one-to-one from ℝⁿ onto
itself, f* is likewise a (finite) differentiable convex function on ℝⁿ which is strictly convex
and co-finite.
Rockafellar, Theorem 26.6: f* is the same as the Legendre conjugate of f, i.e.
f*(x*) = ⟨(∇f)⁻¹(x*), x*⟩ − f((∇f)⁻¹(x*)) for every x*.
Lemma 26.7 #
Rockafellar, Lemma 26.7. Let f be a differentiable convex function on ℝⁿ. In order that
f be co-finite, it is necessary and sufficient that |∇f(xᵢ)| → +∞ for every sequence with
|xᵢ| → +∞.