Convergence of gradients

If convex functions, finite and differentiable on an open convex set, converge pointwise there to a function that is also finite and differentiable, then their gradients converge too, and uniformly on every compact subset. For arbitrary differentiable functions this is false. Convexity is what makes it work, through the upper semicontinuity of the subdifferential under pointwise convergence: both subdifferentials are singletons, so an inclusion ∂fᵢ x ⊆ ∂f x + εB is a bound on ‖∇fᵢ x - ∇f x‖.

Main results

• dist_le_of_subgradient_subset — an inclusion ∂p u ⊆ ∂q v + ε B between singleton subdifferentials is the bound ‖∇p u - ∇q v‖ ≤ ε.
• tendsto_of_hasGradientAt, tendstoUniformlyOn_fderiv_toReal — convergence of the gradients, pointwise and uniformly on every compact subset (Theorem 25.7 in [^1]).

Implementation notes

Subgradients are taken for the pairing innerₗ E, where they are vectors, while a gradient lives in StrongDual ℝ E. The Riesz isomorphism translates between the two, and being an isometry it costs no constant.

References

[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §25.

theorem Tdaf.ConvexAnalysis.dist_le_of_subgradient_subset {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {p q : E → EReal} {u v : E} {a b : StrongDual ℝ E} {ε : ℝ} (hp : ConvexFn p) (hq : ConvexFn q) (ha : HasGradientAt p a u) (hb : HasGradientAt q b v) (hsub : subgradient (innerₗ E) p u ⊆ subgradient (innerₗ E) q v + Metric.closedBall 0 ε) : dist a b ≤ ε

An inclusion of singleton subdifferentials is a bound on gradients: if a is the only subgradient of p at u, b the only one of q at v, and ∂p u ⊆ ∂q v + ε B, then ‖a - b‖ ≤ ε.

theorem Tdaf.ConvexAnalysis.tendsto_of_hasGradientAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : ℕ → E → EReal} {g : E → EReal} {U : Set E} {x : E} (hU : IsOpen U) (hUc : Convex ℝ U) (hf : ∀ (i : ℕ), ConvexFn (f i)) (hfp : ∀ (i : ℕ), Proper (f i)) (hfU : ∀ (i : ℕ), U ⊆ dom (f i)) (hg : ConvexFn g) (hgp : Proper g) (hgU : U ⊆ dom g) (hconv : ∀ z ∈ U, Filter.Tendsto (fun (i : ℕ) => f i z) Filter.atTop (nhds (g z))) (hx : x ∈ U) {G : ℕ → StrongDual ℝ E} {G' : StrongDual ℝ E} (hG : ∀ (i : ℕ), HasGradientAt (f i) (G i) x) (hG' : HasGradientAt g G' x) : Filter.Tendsto G Filter.atTop (nhds G')

The gradients of convex functions converging pointwise on an open convex set converge at every point of it — upper semicontinuity of the subdifferential at the constant sequence xᵢ = x.

theorem Tdaf.ConvexAnalysis.tendstoUniformlyOn_fderiv_toReal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : ℕ → E → EReal} {g : E → EReal} {U : Set E} (hU : IsOpen U) (hUc : Convex ℝ U) (hf : ∀ (i : ℕ), ConvexFn (f i)) (hfp : ∀ (i : ℕ), Proper (f i)) (hfU : ∀ (i : ℕ), U ⊆ dom (f i)) (hg : ConvexFn g) (hgp : Proper g) (hgU : U ⊆ dom g) (hconv : ∀ z ∈ U, Filter.Tendsto (fun (i : ℕ) => f i z) Filter.atTop (nhds (g z))) (hfd : ∀ (i : ℕ), ∀ z ∈ U, DifferentiableAtFn (f i) z) (hgd : ∀ z ∈ U, DifferentiableAtFn g z) {S : Set E} (hS : IsCompact S) (hSU : S ⊆ U) : TendstoUniformlyOn (fun (i : ℕ) => fderiv ℝ fun (w : E) => (f i w).toReal) (fderiv ℝ fun (w : E) => (g w).toReal) Filter.atTop S

Uniform clause: on every compact subset of the open set the gradients converge uniformly. A failure gives points zₙ of the compact set with ‖∇f zₙ - ∇f_{φ n} zₙ‖ ≥ ε; a convergent subsequence zₙ → w turns the subdifferential inclusion along the subsequence and the upper semicontinuity of ∂g at w into two ε/3 bounds that contradict it.