Convergence of directional derivatives and of subgradients #
Convex functions f i, finite on an open convex set U and converging pointwise there to g,
converge uniformly on compact subsets, hence continuously: f i (x i) → g x along any x i → x
in U. Differentiation does not pass to the limit; only the one-sided limsup inequality
survives. For x i → x in U and y i → y,
limsup_i (f i)'(x i; y i) ≤ g'(x; y), ∂(f i)(x i) ⊆ ∂g(x) + ε B eventually.
Equality can fail: for f i x = |x|^{p i} with p i ↓ 1 on U = ℝ, every (f i)'(0; 1) is 0
while g'(0; 1) = 1. Taking the family constant turns the two statements into upper semicontinuity
of f'(x; y) in (x, y) and of ∂f in x.
Main results #
tendsto_eval_of_tendsto— continuous convergence:f i (x i) → g x.eventually_dirDeriv_lt,eventually_subgradient_subset_add_closedBall— the two displayed statements (Theorem 24.5 in [^1]). The first is spelled without junk values: every realμaboveg'(x; y)eventually bounds(f i)'(x i; y i).upperSemicontinuousAt_dirDeriv,eventually_nhds_subgradient_subset_add_closedBall— the constant-family case: upper semicontinuity off'(x; y)and of∂f.eventually_dirDeriv_lt_of_tendsto_dir,eventually_subgradient_subset_exposed_add_closedBall— the same two statements (Theorem 24.6 in [^1]) for an approach to a point ofdom fthat need not be interior, along a fixed limiting directiony, with the face of∂f xexposed byyin place of∂f x.subgradient_dirDeriv— the identification∂(f'(x; ·))(y) = ∂f(x)_y.
Implementation notes #
The convergence theory is stated for real-valued ConvexOn ℝ U (f i) while subgradients are
EReal-valued; the bridge is ConvexFn.convexOn_toReal_dom. ε B needs a norm on the dual side,
so the subgradient statements are for a real inner-product space paired with itself.
Two classical hypotheses are absent: the sequence need not lie in U, only converge to a point of
it, and the approach to a boundary point needs neither closedness of f nor the usual simplex
construction — monotonicity of the difference quotient in its step replaces the vanishing step
‖x i - x‖ by a fixed larger one, after which only continuity at interior points is used.
References #
[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §24.
Support function of a ball #
The support function of the ball of radius ε about the origin is ε ‖·‖.
The directional derivative at an interior point #
At an interior point of dom f the directional derivative is finite in every direction, so it
is the coercion of its own real value.
At an interior point of dom f the directional derivative is a finite convex function on the
whole space.
Positive homogeneity of the directional derivative, read on real values.
Continuous convergence #
Convex functions converging pointwise on an open convex set converge continuously there:
the values f i (x i) along any sequence x i → x converge to g x. This is the practical form of
the fact that pointwise convergence of convex functions is uniform on compact subsets.
Upper semicontinuity of the directional derivative #
Directional derivatives are upper semicontinuous under pointwise convergence. If convex
functions f i, finite on an open convex U, converge pointwise there to g, and if
x i → x ∈ U and y i → y, then
limsup_i (f i)'(x i; y i) ≤ g'(x; y).
The limsup is spelled without junk values: every real μ above g'(x; y) eventually bounds
(f i)'(x i; y i).
The local form, for a single function #
f'(x; y) is upper semicontinuous in (x, y) on int (dom f) × E. This
is the previous theorem for the constant sequence f, f, f, …, transported from sequences to the
neighbourhood filter.
Upper semicontinuity of the subdifferential #
The support function of ∂f x is f'(x; ·), for a real inner-product space paired with
itself, a special case of the same identity for an arbitrary pairing.
The support-function endgame shared by the two subgradient statements below. If the directional
derivative of p at an interior point u of dom p is dominated on the unit ball by that of q
at an interior point v of dom q, up to ε, then ∂p u ⊆ ∂q v + ε B. Positive homogeneity
spreads the bound to every direction, and support functions order closed convex sets.
Subdifferentials are upper semicontinuous under pointwise convergence. If convex functions
f i, finite on an open convex U, converge pointwise there to g, and x i → x inside U,
then for every ε > 0
∂(f i)(x i) ⊆ ∂g(x) + ε B
for all large i, where B is the closed unit ball. The subdifferentials are the support sets of
the directional derivatives, and the previous theorem bounds those pointwise; the bound is made
uniform on the compact unit ball and then spread by positive homogeneity.
The local form of the subgradient statement #
∂f is upper semicontinuous at every interior point of dom f, so that
∂f z ⊆ ∂f x + ε B for all z in a neighbourhood of x.
Approach to a point of the domain along a direction #
The segment principle for effective domains: if x ∈ dom f and x + α • u is interior to
dom f, then so is x + t • u for every t in (0, α].
An approach with a limiting direction that points into the interior is eventually interior: if
x i → x ∈ dom f with x i ≠ x, the unit vectors ‖x i - x‖⁻¹ (x i - x) converge to y, and
x + α y is interior to dom f for some α > 0, then x i ∈ int (dom f) for all large i. This
is what makes the subgradient half of the boundary statement reachable: the sublinear functions
f'(x i; ·) are then finite everywhere, so the uniform-convergence theory applies to them.
A ray into the interior makes the direction interior to the domain of f'(x; ·): if
x + α • y is interior to dom f for some α > 0, then y is interior to dom f'(x; ·),
because a single difference quotient bounds f'(x; ·) above near y.
f'(x; ·) is proper once it is finite at one interior point of its effective domain. A
convex function that takes the value -∞ takes it throughout the relative interior of its domain,
so a single finite interior value rules -∞ out everywhere.
The directional-derivative half: directional derivatives are upper
semicontinuous along an approach to a point of dom f that need not be interior, provided the
approach has a limiting direction y and the second-order derivative in that direction is the
bound.
If x i → x inside dom f with x i ≠ x and the unit vectors |x i - x|⁻¹ (x i - x) converge to
y, and if f'(x; y) > -∞ while the ray x + ℝ₊ y meets int (dom f), then
limsup_i f'(x i; z) ≤ f'(x; y; z) := (f'(x; ·))'(y; z), ∀ z.
As in eventually_dirDeriv_lt the limsup is spelled without junk values: every real μ above
f'(x; y; z) eventually bounds f'(x i; z).
The face of ∂f x exposed by a direction #
The subdifferential of f'(x; ·) at y is the face ∂f(x)_y of ∂f x exposed by y — the
set of subgradients at which ⟨y, ·⟩ attains its maximum over ∂f x. This is the set appearing in
the subgradient half of the boundary statement below, and it composes the support-function
description of f'(x; ·) with the conjugacy characterisation of ∂. Properness of f'(x; ·) is
what makes ∂f x non-empty, so it is not a separate hypothesis.
∂f(x)_y as a normal-cone condition: the subgradients at which y is normal to
∂f x. This is subgradient_dirDeriv read through the definition of the normal cone.
∂(f'(x; ·))(y) is an exposed face of ∂f x, in Mathlib's sense: it is cut out of ∂f x
by maximising the continuous linear functional ⟨y, ·⟩. Composing with IsExposed.isFace makes it
a face of ∂f x in the convex-geometry sense.
The subgradient half of the boundary statement #
The subgradient half: along an approach to a point of dom f with a limiting
direction y pointing into int (dom f), the subdifferentials collapse onto the face of ∂f x
exposed by y,
∂f(x i) ⊆ ∂f(x)_y + ε B eventually,
where ∂f(x)_y = {v ∈ ∂f x | ⟨y, ·⟩ is maximised over ∂f x at v}, identified with ∂(f'(x; ·))(y)
by subgradient_dirDeriv. The argument is that of the interior subgradient statement with
f'(x; ·) replaced by f'(x; y; ·); the step usually left implicit is
eventually_mem_interior_dom_of_tendsto_dir, which makes the f'(x i; ·) finite everywhere.