Rockafellar, §24: Differential Continuity and Monotonicity #
The continuity and monotonicity properties of ∂f, first on the line and then on ℝⁿ, ending with
the characterisation of the subdifferentials as the maximal cyclically monotone mappings.
All eleven numbered results of §24 are formalized: Theorems 24.1–24.9 and Corollaries 24.2.1, 24.5.1.
Two ambient spaces. Theorems 24.1–24.3 are about a closed proper convex function on R, and
are stated here over ℝ itself rather than over Rn 1: that is the book's own reading, since a
one-sided derivative, a non-decreasing function and a subset of R² are real-analytic objects
rather than coordinate ones. The pairing on the line is innerₗ ℝ, which is multiplication.
Theorems 24.4–24.9 are over Rn n with pairing n.
f'₊ and f'₋ are the backbone's rightDeriv and leftDeriv, whose definitions already carry
Rockafellar's extension by +∞ to the right of dom f and -∞ to the left, so nothing here
case-splits on the position of x. Where f is finite the guard is inert, and f'₊(x) = f'(x; 1),
f'₋(x) = -f'(x; -1).
The book gives two descriptions of a complete non-decreasing curve in R²: as
Γ = {(x, x*) | φ₋(x) ≤ x* ≤ φ₊(x)} for a non-decreasing φ not everywhere infinite, and as a
maximal totally ordered subset of R² for the coordinatewise ordering. The second is taken here as
IsCompleteNonDecreasingCurve, Mathlib's IsMaxChain (· ≤ ·) on ℝ × ℝ; the first is the
backbone's monotoneCurve, and isCompleteNonDecreasingCurve_iff_exists_monotone is the
equivalence, which the book asserts without proof.
Maximal cyclic monotonicity is not maximal monotonicity. Rockafellar warns explicitly that
Corollary 31.5.2 does not follow from Theorem 24.9 together with "cyclically monotone implies
monotone", since a mapping maximal in the smaller class need not be maximal in the larger. So
theorem_24_9 is about maximal cyclic monotonicity only, isMonotoneRel_subgradientRel_rn about
plain monotonicity, and nothing here bridges them. On the line the two classes do coincide
(isMonotoneRel_iff_isCyclicallyMonotone_line), which is why Theorem 24.3 can speak of maximal
chains at all.
References #
- R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §24.
Theorem 24.1: the one-sided derivatives on the line #
Theorem 24.1: f'₊ is non-decreasing on R. Closedness is not needed here nor in the next
three clauses: the interlacing chain is an inequality between difference quotients.
Rockafellar, Theorem 24.1: f'₋ is a non-decreasing function on R.
Theorem 24.1: f'₊ and f'₋ are finite exactly on int (dom f). The book says "finite on
the interior"; the biconditional says slightly more, that finiteness characterises it.
Rockafellar, Theorem 24.1, the interlacing chain:
f'₊(z₁) ≤ f'₋(x) ≤ f'₊(x) ≤ f'₋(z₂) when z₁ < x < z₂.
Theorem 24.1, first limit formula: lim_{z ↓ x} f'₊(z) = f'₊(x). Closedness is essential
here and in the three companions: for the proper convex f that is 1 at 0, 0 on (0, ∞) and
+∞ on (-∞, 0), f'₊ is -∞ at 0 and 0 to the right of it.
Rockafellar, Theorem 24.1, second limit formula: lim_{z ↑ x} f'₊(z) = f'₋(x).
Rockafellar, Theorem 24.1, third limit formula: lim_{z ↓ x} f'₋(z) = f'₊(x).
Rockafellar, Theorem 24.1, fourth limit formula: lim_{z ↑ x} f'₋(z) = f'₋(x).
§24, the remark after Theorem 24.1: ∂f(x) = {x* ∈ R | f'₋(x) ≤ x* ≤ f'₊(x)}. Only
properness is needed.
Theorem 24.2 and Corollary 24.2.1: the primitive of a non-decreasing function #
Theorem 24.2, existence with the identification of the one-sided derivatives: for a
non-decreasing φ finite at a there is a closed proper convex f on R with f'₋ = φ₋ and
f'₊ = φ₊, where φ₋(x) = lim_{z ↑ x} φ(z) and φ₊(x) = lim_{z ↓ x} φ(z). The book exhibits f
as ∫ₐˣ φ(t) dt; here it is built from the graph Γ(φ), a maximal monotone relation.
Theorem 24.2, uniqueness: two closed proper convex functions on R squeezed around the
same φ differ by a constant. The two squeezes force ∂f = ∂g, and a subdifferential determines a
closed proper convex function up to an additive constant.
Theorem 24.2 as the book states it, minus the integral formula: for a non-decreasing φ
finite at a there is a closed proper convex f on R with f'₋ ≤ φ ≤ f'₊, unique up to an
additive constant.
Corollary 24.2.1, right-derivative half: on the interior of its effective domain a proper
convex function on R is the integral of f'₊,
f(y) - f(x) = ∫ₓʸ f'₊(t) dt.
The integrand is the derivative of a function already convex and finite on an open interval, so this is the fundamental theorem of calculus and needs no theory of monotone functions.
Corollary 24.2.1, left-derivative half: f(y) - f(x) = ∫ₓʸ f'₋(t) dt. The two one-sided
derivatives differ only on the jump set of f'₊, which is countable and hence null.
Theorem 24.3: the complete non-decreasing curves #
§24. A complete non-decreasing curve in R² is a maximal totally ordered subset for
the coordinatewise partial ordering — a maximal chain. The book introduces the notion by the
formula Γ = {(x, x*) | φ₋(x) ≤ x* ≤ φ₊(x)} and then records this description as equivalent.
Equations
- Rockafellar.IsCompleteNonDecreasingCurve Γ = IsMaxChain (fun (x1 x2 : ℝ × ℝ) => x1 ≤ x2) Γ
Instances For
The bridge to the backbone: a maximal chain of ℝ × ℝ is exactly a maximal monotone
relation on the line. Monotonicity of a relation on R is total ordering of its graph, the only
difference being that IsChain excuses the diagonal, which le_refl supplies.
§24, the book's defining formula implies the order-theoretic description: the region between
the two one-sided limits of a non-decreasing φ that is finite somewhere is a complete
non-decreasing curve. Maximality of Γ(φ) is what produces the primitive in Theorem 24.2.
Rockafellar, Theorem 24.3: the graphs of the subdifferential mappings of the closed proper
convex functions on R are precisely the complete non-decreasing curves in R².
§24, the converse: every complete non-decreasing curve is the region between the two
one-sided limits of a non-decreasing φ that is finite somewhere. Theorem 24.3 turns the maximal
chain into a subdifferential, which is the curve of the right derivative with its value at one
relative interior point of the domain replaced by a subgradient there.
§24: the book's two descriptions of a complete non-decreasing curve agree. The book states the order-theoretic one without proof, immediately after the defining formula.
Theorem 24.3, second clause: f is determined by Γ up to an additive constant. The
backbone needs only the inclusion ∂f ⊆ ∂g, which is what Theorem 24.9's maximality argument
consumes.
Theorem 24.3, the converse direction in the book's own vocabulary: the graph of ∂f is
the region between the two one-sided limits of f'₊.
§24, the remark after Theorem 24.3: if Γ is a complete non-decreasing curve then so is
Γ* = {(x*, x) | (x, x*) ∈ Γ}. The book proves it by conjugacy, Γ* = graph ∂f*;
order-theoretically it is free, Prod.swap being an order isomorphism of ℝ × ℝ.
Theorem 24.4: the graph of ∂f is closed #
Theorem 24.4: the graph of ∂f is a closed subset of Rⁿ × Rⁿ. Convexity is not used,
and closedness of f enters only through lower semicontinuity: the book's proof runs through
Theorem 23.5 and the conjugate, whereas the graph is written here as an intersection of preimages
of epi f.
Rockafellar, Theorem 24.4 in the book's own words: if xᵢ* ∈ ∂f(xᵢ) with xᵢ → x and
xᵢ* → x*, then x* ∈ ∂f(x).
Theorem 24.5 and Corollary 24.5.1: convergence of directional derivatives #
Theorem 24.5, first assertion without junk values: every real μ above f'(x; y)
eventually bounds fᵢ'(xᵢ; yᵢ). This is the book's limsup inequality with the extended-real limit
superior replaced by its defining property; theorem_24_5_limsup is the literal statement. The
hypotheses are the book's — the fᵢ and g convex on Rⁿ and finite on the open convex C.
Theorem 24.5, first assertion literally: limsup_i fᵢ'(xᵢ; yᵢ) ≤ f'(x; y). Equality can
fail: fᵢ(x) = |x|^{pᵢ} with pᵢ ↓ 1 converges pointwise to |x| on R with every
fᵢ'(0; 1) = 0 while f'(0; 1) = 1.
Rockafellar, Theorem 24.5, second assertion: given ε > 0 there is an index i₀ with
∂fᵢ(xᵢ) ⊆ ∂f(x) + εB for all i ≥ i₀, B the Euclidean unit ball.
Corollary 24.5.1, first assertion: f'(x; y) is upper semicontinuous in
(x, y) ∈ int (dom f) × Rⁿ — the constant sequence in Theorem 24.5. It cannot be strengthened to
continuity in x, though it is continuous in y for each fixed interior x.
Rockafellar, Corollary 24.5.1, second assertion: for x ∈ int (dom f) and ε > 0 there is
a δ > 0 with ∂f(z) ⊆ ∂f(x) + εB for every z within δ of x.
Theorem 24.6: approach to a point of dom f along a direction #
§24. ∂f(x)_y is the set of points x* ∈ ∂f(x) at which y is normal to ∂f(x);
equivalently (subgradientNormal_eq_sep) the face of ∂f(x) exposed by y.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The bridge: y is normal to a set at v exactly when v maximises ⟨y, ·⟩ over it.
Theorem 24.6, first assertion without junk values: every real μ above the second-order
derivative f'(x; y; z) = dirDeriv (dirDeriv f x) y z eventually bounds f'(xᵢ; z). Rockafellar
assumes f closed; that is not needed here, because the vanishing step |xᵢ - x| is replaced by a
fixed larger one, so only continuity of f at interior points is used.
Rockafellar, Theorem 24.6, first assertion, literally:
limsup_i f'(xᵢ; z) ≤ f'(x; y; z) for every z.
Rockafellar, Theorem 24.6, second assertion: given ε > 0 there is an index i₀ with
∂f(xᵢ) ⊆ ∂f(x)_y + εB for all i ≥ i₀.
Theorem 24.7: local boundedness of ∂f and the Lipschitz property #
Theorem 24.7, quantitative half: a single α bounds the subgradients over a compact
S ⊆ int (dom f), bounds the directional derivatives there, and is a Lipschitz constant for f on
S. The book takes α = sup {|x*| : x* ∈ ∂f(S)}; what is asserted here is the existence of some
such α, which is implied by, but weaker than, the book's sharper reading.
Rockafellar, Theorem 24.7: ∂f(S) = ⋃ {∂f(x) | x ∈ S} is non-empty for a non-empty
S ⊆ int (dom f). This is Theorem 23.4 applied at any point of S.
Rockafellar, Theorem 24.7, topological half: ∂f(S) is compact for a closed proper convex
f and a compact S ⊆ int (dom f). Closedness of ∂f(S) is Theorem 24.4.
Rockafellar, Theorem 24.7: ∂f(S) is closed.
Rockafellar, Theorem 24.7: ∂f(S) is bounded.
Theorems 24.8 and 24.9: cyclic monotonicity #
Theorem 24.8, sufficiency: a cyclically monotone multivalued mapping from Rⁿ to Rⁿ is
contained in the subdifferential of a closed proper convex function. The empty mapping is included,
which Rockafellar's own proof excludes by fiat.
Rockafellar, Theorem 24.8: a multivalued mapping from Rⁿ to Rⁿ is contained in the
subdifferential of a closed proper convex function if and only if it is cyclically monotone.
Theorem 24.9, one half: the subdifferential of a closed proper convex function is a maximal cyclically monotone mapping — not a statement about maximal monotonicity.
Rockafellar, Theorem 24.9: the subdifferential mappings of the closed proper convex
functions on Rⁿ are exactly the maximal cyclically monotone mappings from Rⁿ to Rⁿ.
Theorem 24.9, second clause: the function is determined by its subdifferential mapping up
to an additive constant. The backbone assumes only the inclusion ∂f ⊆ ∂g.
§24: ∂f is a monotone mapping, the case m = 1 of cyclic monotonicity. Kept deliberately
separate from theorem_24_9: maximal monotonicity of ∂f, Corollary 31.5.2, does not follow
from Theorem 24.9 together with "cyclically monotone implies monotone".
§24: when n = 1 the monotone and the cyclically monotone mappings are the same. The book
derives this from Theorems 24.3 and 24.9; the proof here rotates a cycle so that the pair
maximising x + x* comes first and deletes it. For n > 1 it is false: a linear ρ with matrix
Q is monotone as soon as the symmetric part of Q is positive semi-definite, and cyclically
monotone only if Q itself is symmetric.