Directional derivatives and subgradients of a saddle-function #
The one-variable differential theory of convex functions, read for a concave-convex function of a
pair on an open rectangle C ×ˢ D where the function is finite and real-valued.
The joint one-sided directional derivative exists and splits,
K'(u, v; u', v') = K'(u, v; u', 0) + K'(u, v; 0, v'), and is a finite concave-convex function of
the direction. The subdifferential ∂K = ∂₁K ×ˢ ∂₂K is a product — the two variables never
interact — so differentiability is a separate condition in each variable: K is differentiable
at a point exactly when ∂K is a singleton there. The directional derivatives are semicontinuous
and ∂K upper semicontinuous along a convergent sequence.
Main definitions #
dirDerivReal f x y— the one-sided directional derivativef'(x; y)of a real-valued function, read as a genuine limit and taking the junk value0where that limit fails to exist.subgradientFst,subgradientSnd,subgradientSaddle—∂₁K,∂₂Kand∂K = ∂₁K ×ˢ ∂₂K.prodInnerL q— the functional(w, x) ↦ ⟪w, q.1⟫ + ⟪x, q.2⟫that a pair represents;HasSaddleGradientAt K q pisHasFDerivAt K (prodInnerL q) p.
Main results #
dirDerivReal_prod,tendsto_slope_dirDerivReal_prod,concaveConvexOn_dirDerivReal— the joint limit exists, splits into the two partial derivatives, and is a finite concave-convex function of the direction (Theorem 35.6 in [^1]).eventually_dirDerivReal_snd_lt,eventually_lt_dirDerivReal_fst,eventually_subgradientSaddle_subset— the two semicontinuity inequalities, spelled without junk values, and∂K_i(u_i, v_i) ⊆ ∂K(u, v) + εBeventually (Theorem 35.7 in [^1]).lowerSemicontinuousAt_dirDerivReal_fst,upperSemicontinuousAt_dirDerivReal_snd,eventually_nhds_subgradientSaddle_subset— the same for the constant sequence, that is, plain semicontinuity on the rectangle.hasSaddleGradientAt_iff_subgradientSaddle_eq_singleton,differentiableAt_iff_exists_subgradientSaddle_eq_singleton— differentiability is unique subdifferentiability (Theorem 35.8 in [^1]).differentiableAt_iff_isLinearMap_dirDerivReal— whereKis already finite, differentiability is exactly linearity ofK'(u, v; ·, ·).
Four one-variable statements are proved here in real form, each with its concave mirror, because
the EReal versions are not usable through a slice without a detour: the gradient inequality and
its uniqueness half, the description of ∂f(x) by the directional derivative at an interior point,
and nonemptiness of ∂f(x) there.
Implementation notes #
subgradientFst and subgradientSnd test against C and D rather than the whole space;
Rockafellar tests against Rᵐ, the case C = univ, and the two agree once K is extended off the
rectangle by the simple extension of Saddle/Kernel.lean.
Mathlib gives U × X the supremum norm, so it is not an inner-product space and ∇K (u, v) has
to be a pair rather than a vector; the same choice makes the εB of the semicontinuity statements
the supremum ball rather than the book's Euclidean one, harmlessly, since every statement
quantifies over all ε > 0. Everything is stated on an open rectangle, as in the book.
References #
[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §35.
The one-sided directional derivative of a real-valued function #
The one-sided directional derivative f'(x; y) of a real-valued function: the limit of the
difference quotient as the step decreases to 0, with the junk value 0 where it does not exist.
dirDeriv (Subgradient/Defs.lean) is an infimum instead, which agrees with the limit only when
the quotient is monotone in the step — true along a line for a convex function, false for a
saddle-function in a joint direction, which is the case treated here.
Equations
- Tdaf.ConvexAnalysis.dirDerivReal f x y = (nhdsWithin 0 (Set.Ioi 0)).limUnder fun (t : ℝ) => (f (x + t • y) - f x) / t
Instances For
Reading off dirDerivReal from a limit that is known to exist.
At a point where a convex function is finite on a neighbourhood, the one-sided difference
quotient converges. It is the secant slope along the line t ↦ x + t • y, nondecreasing and
bounded below by its value at a negative step, so it converges to its infimum.
The same for a concave function: the one-sided difference quotient converges.
The difference quotient of a convex function converges to dirDerivReal.
The difference quotient of a concave function converges to dirDerivReal.
Positive homogeneity, in the form that transports a limit. No convexity is involved: it is
the reparametrisation t ↦ t * c of the difference quotient.
Positive homogeneity of f'(x; ·), wherever the limit defining it exists.
f'(x; 0) = 0, with no hypothesis: the difference quotient is identically 0.
Convexity of the directional derivative in the direction #
The affine identity behind every restriction to a line: for a + b = 1 the point
x + t • (a • d₁ + b • d₂) is the corresponding convex combination of x + t • d₁ and
x + t • d₂.
Every direction eventually stays inside an open set.
f'(x; ·) is a convex function of the direction on the whole space, when f is convex on
an open set containing x.
The difference quotient is convex in the direction for every fixed step, by the affine identity
add_smul_convexComb together with the convexity of f; the inequality survives the limit.
The mirror: f'(x; ·) is a concave function of the direction.
The directional derivative of a convex function is bounded above by every difference
quotient whose step keeps the point inside the set on which f is convex.
The quotient is nondecreasing in the step, so the limit at 0 is below the value at step α.
The concave counterpart of dirDerivReal_le_slope.
The joint directional derivative of a saddle-function #
Negating a concave-convex function and swapping its arguments gives a concave-convex function
of the swapped pair: (x, w) ↦ -K (w, x) is concave-convex on D × C.
This involution is what makes the two halves of the joint limit below a single statement: the
liminf half for K is the limsup half for the swap.
The limsup half: moving the concave variable does not raise the difference quotient of
the convex variable above its limit at the base point.
Given μ above K'(u, v; 0, v'), some step α > 0 already realises a secant slope of the convex
slice below μ; the concave slice is continuous along t ↦ u + t • u', so the same secant slope at
the moving point is still below μ for small t.
The joint one-sided directional derivative of a finite concave-convex function at an interior point of the rectangle exists, and it is the sum of the two partial directional derivatives.
The difference quotient splits as
[K(u + t u', v) - K(u, v)]/t + [K(u + t u', v + t v') - K(u + t u', v)]/t, whose first summand
converges by the one-variable existence clause. eventually_slope_snd_lt bounds the second above
by anything above K'(u, v; 0, v'), and the matching lower bound is that lemma at the negated
swap.
The joint directional derivative in terms of dirDerivReal #
The joint difference quotient of a finite concave-convex function converges, and its limit is
dirDerivReal K (u, v) q.
This is tendsto_slope_prod with the two partial limits supplied by
tendsto_slope_dirDerivReal_of_concaveOn and ..._of_convexOn.
The splitting of the joint directional derivative:
K'(u, v; u', v') = K'(u, v; u', 0) + K'(u, v; 0, v').
K'(u, v; ·, ·) is a finite concave-convex function on the whole of U × X.
By the splitting it is the sum of a concave function of the first direction and a convex function
of the second, and each summand is finite because the corresponding slice of K is finite on a
neighbourhood of the base point.
The homogeneity clause: K'(u, v; ·, ·) is positively homogeneous.
Read on the first axis: the joint directional derivative in a direction of the form (u', 0)
is the partial one, K'(u, v; u', 0).
Read on the second axis: the joint derivative at (0, v') is K'(u, v; 0, v').
The subdifferential of a saddle-function #
∂₁K(u, v), the subdifferential of a saddle-function in its concave variable: the
supergradients at u of the concave slice K (·, v), tested against the points of C.
Rockafellar tests against all of Rᵐ, which is the case C = univ.
Equations
Instances For
∂₂K(u, v): the subgradients at v of the convex slice K (u, ·), tested against D.
Equations
Instances For
∂K(u, v) = ∂₁K(u, v) × ∂₂K(u, v), Rockafellar's subdifferential of a saddle-function.
It is a product, not a set of joint subgradients: the two variables never interact, which is what makes differentiability a condition on each variable separately.
Equations
Instances For
∂₂K(u, v) is the subdifferential, in the sense of Subgradient/Defs.lean, of the convex
slice extended by +∞ off D. This is the bridge that lets the one-variable subgradient theory be
applied to a saddle-function one variable at a time.
∂₁K(u, v) is the negated subdifferential of the negated concave slice extended by +∞ off
C: the concave variable reaches the convex theory through -K.
Continuous convergence, and semicontinuity of the directional derivatives #
Finite concave-convex functions converge continuously. Pointwise convergence on an open
convex rectangle C × D forces K i (u i, v i) → K (u, v) along every sequence
(u i, v i) → (u, v) in C × D. This combines uniform convergence on compact rectangles with
continuity of the limit, on a closed-ball rectangle.
The directional derivatives in the convex variable are upper semicontinuous along the
convergence,
limsup_i K_i'(u_i, v_i; 0, v') ≤ K'(u, v; 0, v').
Spelled without junk values: every real μ above K'(u, v; 0, v') eventually bounds
K_i'(u_i, v_i; 0, v'). A single step α > 0 realises a secant slope of K (u, ·) below μ;
continuous convergence carries that slope to K i at the moving points; and the directional
derivative is below every secant slope.
The directional derivatives in the concave variable are lower semicontinuous along the
convergence,
liminf_i K_i'(u_i, v_i; u', 0) ≥ K'(u, v; u', 0).
This is eventually_dirDerivReal_snd_lt read for the negated swap; it is proved here directly
because the roles of the two sequences do not swap.
Upper semicontinuity of the subdifferentials #
Negating a set thickened by a ball thickens the negated set by the same ball: the closed ball about the origin is symmetric.
A product of thickened sets is contained in the thickening of the product.
In the convex variable: ∂₂K_i(u_i, v_i) ⊆ ∂₂K(u, v) + εB eventually.
Upper semicontinuity of the one-variable subdifferential, applied to the convex slices
K_i (u_i, ·) extended by +∞ off D; the family converges pointwise on D to K (u, ·) by
continuous convergence.
In the concave variable: ∂₁K_i(u_i, v_i) ⊆ ∂₁K(u, v) + εB eventually.
The same argument through -K: ∂₁ is the negated subdifferential of the negated concave slice,
and negation carries the ε-thickening across because the ball is symmetric.
∂K_i(u_i, v_i) ⊆ ∂K(u, v) + εB eventually, with B the unit ball of U × X.
The subdifferential of a saddle-function is the product of the two one-variable ones, and the
unit ball of a product is the product of the unit balls (Metric.closedBall_prod_same), so the
statement is the conjunction of the previous two.
The constant sequence: semicontinuity on the rectangle #
K'(u, v; u', 0) is lower semicontinuous in (u, v) on C × D.
The sequential statement for the constant sequence K, K, K, …, transported from sequences to the
neighbourhood filter (𝓝 (u, v) is countably generated).
K'(u, v; 0, v') is upper semicontinuous in (u, v) on C × D.
∂K is upper semicontinuous on C × D: ∂K(x, y) ⊆ ∂K(u, v) + εB for every (x, y) near
(u, v).
Tangent inequalities at a point of differentiability #
Where a real-valued function is Fréchet differentiable, dirDerivReal is the value of the
derivative in the given direction.
The gradient inequality: a convex function on an open set lies above its tangent at a point of differentiability.
The difference quotient is nondecreasing in the step, so its limit at 0 — the derivative — is
below its value at step 1, which is f z - f x.
The gradient inequality for a concave function: it lies below its tangent.
A linear function that minorises the increment of f is the derivative. No convexity is
used — only the limit of the difference quotient along the two opposite rays.
The same for a concave function: a linear majorant of the increment is the derivative.
The gradient of a saddle-function, as a pair #
The continuous linear functional on U × X represented by a pair q = (u*, v*), namely
(w, x) ↦ ⟪w, u*⟫ + ⟪x, v*⟫.
A product of inner-product spaces carries the supremum norm in Mathlib, so U × X is not itself
an inner-product space and Mathlib's gradient does not apply to a function of a pair.
Rockafellar's ∇K (u, v) is the pair q for which prodInnerL q is the Fréchet derivative.
Equations
- Tdaf.ConvexAnalysis.prodInnerL q = (innerSL ℝ) q.1 ∘SL ContinuousLinearMap.fst ℝ U X + (innerSL ℝ) q.2 ∘SL ContinuousLinearMap.snd ℝ U X
Instances For
∇K p = q: K is Fréchet differentiable at p with derivative prodInnerL q. This is
Rockafellar's gradient of a finite saddle-function, split into its two blocks.
Equations
Instances For
A saddle-function with a gradient is differentiable.
The concave slice of a differentiable saddle-function is differentiable, with the first block of the gradient as its derivative.
The convex slice of a differentiable saddle-function is differentiable, with the second block of the gradient as its derivative.
In finite dimensions every continuous linear functional on U × X is a prodInnerL, by the
Riesz representation in each factor.
In finite dimensions, being differentiable and having a saddle-gradient are the same.
Thickening a singleton #
Membership in a singleton thickened by a closed ball about the origin is a bound on the distance to that point.
Differentiability and a unique subgradient #
The subdifferential of a saddle-function is a singleton exactly when each of its two blocks is, provided both are nonempty. It is a product, so this is not automatic: an empty factor makes the product empty whatever the other factor is.
At a point where K is differentiable the first block of ∇K is the only element of
∂₁K(u, v).
The same in the convex variable: the second block of ∇K is the only element of
∂₂K(u, v).
Where a finite concave-convex function is differentiable, its gradient is its unique subgradient.
∂₂K(u, v) is nonempty at every point of the open rectangle: a convex function has a
subgradient wherever it is finite on a neighbourhood.
∂₁K(u, v) is nonempty at every point of the open rectangle, by the same fact for the concave
slice.
Upper semicontinuity of ∂₁K on the rectangle, in the concave variable alone.
Upper semicontinuity of ∂₂K on the rectangle, in the convex variable alone.
Converse half: a finite concave-convex function with a unique subgradient at a point of an open rectangle is differentiable there, jointly in the two variables.
The proof is not the book's, which upgrades separate to joint differentiability through uniform
convergence of the rescalings
h_λ (x, y) = [K (u + λx, v + λy) - K (u, v) - λ⟪x, u*⟫ - λ⟪y, v*⟫] / λ. Upper semicontinuity of
∂K gives the estimate outright: the increment K (u + a, v + b) - K (u, v) is sandwiched by
subgradient inequalities at (u, v), (u, v + b) and (u + a, v + b), each of whose subgradients
lies within ε of q, so the error is at most ε (‖a‖ + ‖b‖).
A finite concave-convex function is differentiable at a point of an open rectangle exactly when it has a unique subgradient there, and the gradient is then that subgradient.
The same without naming the gradient: differentiability and unique subdifferentiability are the same property.
Subgradients through the directional derivative, in real form #
An inner product separates points on the right, and a one-sided comparison is enough because directions come in pairs.
y satisfies the subgradient inequality of f at x on S exactly when ⟪w, y⟫ ≤ f'(x; w)
in every direction w.
Rockafellar states it as "cl f'(x; ·) is the support function of ∂f(x)"; at an interior point
of an open set no closure is needed, and this is the pointwise reading.
The concave case: y is a supergradient exactly when f'(x; w) ≤ ⟪w, y⟫ in every direction.
Differentiability is linearity of K'(u, v; ·, ·) #
A partial directional derivative equal to the linear function ⟪·, q.1⟫ pins ∂₁K(u, v) down
to {q.1}, for the concave variable. Unlike the usual Gâteaux criterion this needs no upgrade to
Fréchet differentiability, because its conclusion is about subgradients.
The same for the convex variable: ∂₂K(u, v) is pinned down to {q.2}.
∇K(u, v) = q exactly when K'(u, v; ·, ·) is the linear function prodInnerL q. The forward
direction needs no hypothesis; the converse restricts the identity to the two axes, turns each into
a one-point subdifferential, and invokes the differentiability criterion.
For a concave-convex function already finite on an open rectangle — Rockafellar's "K is
finite on a neighbourhood of (u, v)" — differentiability at (u, v) is exactly linearity of
K'(u, v; ·, ·).
The book's last clause, that finiteness of the m + n two-sided partial derivatives already
suffices, is not formalised: it is a statement about a coordinate basis rather than about the
space.