Rockafellar, §35: Continuity and Differentiability of Saddle-Functions #
The §10 continuity and convergence theorems and the §23/§24/§25 differential theory, read for a concave-convex function of a pair. All twelve numbered results of §35 are formalized: Theorems 35.1–35.10 and Corollaries 35.7.1 and 35.8.1.
The sign asymmetry. K is concave in u and convex in v, so ∂₁K (u, v) holds the
supergradients of the concave slice K (·, v) at u and ∂₂K (u, v) the subgradients of the
convex slice K (u, ·) at v, with ∂K = ∂₁K × ∂₂K. The two inequalities point in opposite
directions, so ∂K is not the subdifferential of K read on ℝᵐ⁺ⁿ, and is not a monotone
relation. The dictionary is mem_subgrad₁_iff_neg_mem_subgradient_neg, and that single u* ↦ -u*
is what §37's Corollary 37.5.2 inserts to recover monotonicity.
K′(u, v; u′, v′) is dirDerivReal K (u, v) (u′, v′), a genuine limit of difference quotients.
The EReal-valued dirDeriv of §23 is an infimum, which is that limit only along a line; the
difference between the two is exactly what Theorem 35.6 is about.
Divergences from the book #
Theorems 35.6–35.10 are stated for a real-valued K on an open rectangle C × D, where the
book's K is EReal-valued on ℝᵐ × ℝⁿ and merely finite on C × D. So ∂₁K and ∂₂K are
tested against C and D rather than all of ℝᵐ and ℝⁿ; subgradFst_univ_eq and its two
companions are the bridge, and the readings agree once K is extended off C × D by the simple
extension, which makes the extra inequalities vacuous.
The εB of Theorems 35.7, 35.9 and 35.10 is the supremum ball, Mathlib's norm on a product. It
differs from the book's Euclidean ball by a factor bounded by √2, and every such statement
quantifies over all ε > 0.
References #
- R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §35, pp. 370–378.
Two bookkeeping steps #
Theorem 35.1 #
Theorem 35.1, first assertion: a finite concave-convex K on C × D, with C and D
relatively open convex, is continuous relative to C × D. "Relatively open" is ri C = C.
Theorem 35.1, second assertion: K is Lipschitzian on every closed bounded subset of
C × D. In ℝᵐ⁺ⁿ such a set is compact and lies in the rectangle spanned by its projections.
Theorem 35.2 #
Theorem 35.2. For C, D relatively open convex and a family of finite concave-convex
functions on C × D that is pointwise bounded on a dense C′ × D′, the family is uniformly
bounded and equi-Lipschitzian relative to every closed bounded subset of C × D. The family is
indexed by an arbitrary type, so it may be empty.
Stated with cl C′ ⊇ C and cl D′ ⊇ D where the book asks for conv (cl (C′ × D′)) ⊇ C × D; the
convex hull is dropped, as Rockafellar.theorem_10_6_ab already does for the one-variable §10.
Theorem 35.3 #
Theorem 35.3. For C, D relatively open convex, T locally compact, and F (u, v, t)
concave in u, convex in v and continuous in t, F is jointly continuous on C × D × T. The
two convex variables are grouped as a pair, since the concave-convex hypothesis lives there.
Theorem 35.3, weakened hypothesis: continuity in t need only hold at the points of dense
subsets C′ and D′.
Theorems 35.4 and 35.5 #
Theorem 35.4. If finite concave-convex K 1, K 2, … on C × D converge to finite limits
on a dense C′ × D′, the limit exists everywhere on C × D, is finite and concave-convex, and the
convergence is uniform on every closed bounded subset of C × D.
Theorem 35.5. With "the limit exists" weakened to "the values are bounded", some subsequence converges to a finite concave-convex function, uniformly on closed bounded subsets. This is Arzelà–Ascoli for saddle-functions; the countable dense set comes from separability.
The subdifferential of a saddle-function #
Rockafellar's definition, for an arbitrary — hence EReal-valued — concave-convex K.
Rockafellar's ∂₁K (u, v) = ∂_u K (u, v): the u* with K (u′, v) ≤ K (u, v) + ⟨u*, u′ - u⟩
for every u′, i.e. the supergradients at u of the concave slice K (·, v). An abbrev for
concaveSubgradient at the Euclidean pairing.
Equations
- Rockafellar.subgrad₁ K p = Tdaf.ConvexAnalysis.concaveSubgradient (TdafSurface.pairing m) (fun (u : TdafSurface.Rn m) => K (u, p.2)) p.1
Instances For
Rockafellar's ∂₂K (u, v) = ∂_v K (u, v): the v* with K (u, v) + ⟨v*, v′ - v⟩ ≤ K (u, v′)
for every v′, i.e. the subgradients at v of the convex slice K (u, ·). The inequality
points the other way from subgrad₁'s; that asymmetry is the whole sign convention.
Equations
- Rockafellar.subgrad₂ K p = Tdaf.ConvexAnalysis.subgradient (TdafSurface.pairing n) (fun (v : TdafSurface.Rn n) => K (p.1, v)) p.2
Instances For
Rockafellar's ∂K (u, v) = ∂₁K (u, v) × ∂₂K (u, v). It is a product, not a set of joint
subgradients, and its two factors carry opposite inequalities, so it is not the subdifferential of
K read as a function on ℝᵐ⁺ⁿ.
Equations
Instances For
∂K (u, v) = ∂₁K (u, v) × ∂₂K (u, v), definitionally.
The defining inequality of ∂₁K (u, v).
The defining inequality of ∂₂K (u, v), pointing the opposite way.
Where the sign flip sits. u* is a supergradient of K (·, v) at u exactly when -u*
is a subgradient of -K (·, v) there. This negation is what §37 inserts in Corollary 37.5.2 to
make the relation monotone and in Corollary 37.5.1 to make the map (u - u*, v* + v).
∂K (u, v) is a convex subset of ℝᵐ × ℝⁿ, with no hypothesis on K at all.
The bridge between the two readings of ∂K #
∂₁ in rectangle-relative form is ∂₁ in the book's global form, at C = ℝᵐ.
∂₂ in rectangle-relative form is ∂₂ in the book's global form, at D = ℝⁿ.
∂K in rectangle-relative form is ∂K in the book's global form, at C × D = ℝᵐ × ℝⁿ.
Theorem 35.6, the splitting identity #
Theorem 35.6, the displayed equation: for K concave-convex and finite on an open
C × D and (u, v) ∈ C × D, K′(u, v; u′, v′) = K′(u, v; u′, 0) + K′(u, v; 0, v′). Convexity of
C and D is not needed — only room around each point in each variable separately.
Theorem 35.6, the existence clause: the joint difference quotient really has a limit, so
K′(u, v; u′, v′) exists. This is the part the book calls "problematical".
Theorem 35.6, the shape clause: K′(u, v; ·, ·) is a finite concave-convex function on
the whole of ℝᵐ × ℝⁿ.
Theorem 35.6, the homogeneity clause: K′(u, v; ·, ·) is positively homogeneous.
Theorem 35.7 and Corollary 35.7.1 #
Theorem 35.7, first inequality: liminf_i K_i′(u_i, v_i; u′, 0) ≥ K′(u, v; u′, 0), spelled
without junk values as: every real μ below the right-hand side eventually falls below
K_i′(u_i, v_i; u′, 0). The step the book leaves out is that finite concave-convex functions
converge continuously, K i (u i, v i) → K (u, v) along a moving sequence.
Theorem 35.7, second inequality: limsup_i K_i′(u_i, v_i; 0, v′) ≤ K′(u, v; 0, v′).
Theorem 35.7, third assertion: given ε > 0 there is an i₀ with
∂K_i (u_i, v_i) ⊆ ∂K (u, v) + εB for all i ≥ i₀.
Corollary 35.7.1, first assertion: for each u′, K′(u, v; u′, 0) is lower
semicontinuous in (u, v) on C × D. It is Theorem 35.7 for the constant sequence.
Corollary 35.7.1, second assertion: for each v′, K′(u, v; 0, v′) is upper
semicontinuous in (u, v) on C × D.
Corollary 35.7.1, third assertion: given (u, v) ∈ C × D and ε > 0 there is a δ > 0
with ∂K (x, y) ⊆ ∂K (u, v) + εB for every (x, y) within δ of (u, v).
Theorem 35.8 and Corollary 35.8.1 #
Theorem 35.8, first half: if K is differentiable at (u, v) then ∇K (u, v) is its
unique subgradient there. HasSaddleGradientAt K q p reads ∇K p = q with q a pair of
vectors, a product of inner-product spaces carrying the supremum norm in Mathlib.
Theorem 35.8: K is differentiable at (u, v) if and only if it has a unique subgradient
there. The converse is proved from Corollary 35.7.1, which gives the Fréchet estimate directly.
Corollary 35.8.1: for K concave-convex and finite on a neighbourhood of (u, v),
differentiability there is exactly linearity of K′(u, v; ·, ·). The corollary's last clause —
that finiteness of the m + n two-sided partial derivatives suffices — is not formalized.
Theorems 35.9 and 35.10 #
Theorem 35.9, measure clause: the set where a finite concave-convex K fails to be
differentiable on C × D is null. Proved from Theorem 35.1 plus Rademacher, as §25 does.
Theorem 35.9, density clause: the set of points of C × D at which K is differentiable
is dense in C × D.
Theorem 35.9, continuity clause: the gradient mapping is continuous on the set where it
exists. There is no canonical ∇K without choice, so the statement takes any G representing it
on S; prodInnerL is injective, so G is unique there, and S = E gives the book.
Theorem 35.10: if finite differentiable concave-convex K i converge pointwise on an open
convex C × D to a finite differentiable concave-convex K, then ∇K i (u, v) → ∇K (u, v).
Differentiability is needed only at the point in question, not everywhere as the book assumes.
Theorem 35.10, last sentence: the gradient mappings converge uniformly on every closed
bounded subset of C × D.