Robustness of the limiting subdifferential (Eq. (3))

Proved

NonconvexSplitting.ProxADMM.limitingSubdiff_robust

by mikedeng1 · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

p2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1variational-analysis

Let $f : \mathbb{R}^m \to (-\infty, +\infty]$ be proper, and let $u \in \mathbb{R}^m$ with $f(u) < +\infty$ . Suppose $u^t \to u$ with $f(u^t) \to f(u)$ , $v^t \to v$ , and $v^t \in \partial f(u^t)$ for every $t$ , where $\partial$ is the limiting subdifferential. Then

v \in \partial f(u).

Equivalently, $\{v : \exists\, u^t \xrightarrow{f} u,\ v^t \to v,\ v^t \in \partial f(u^t)\} \subseteq \partial f(u)$ : the graph of $\partial f$ is closed along $f$ -attentive sequences.

This is the property used to pass to the limit in the optimality conditions of the ADMM subproblems.

Preamble

import Mathlib
import Definitions.Def_NonconvexSplitting_Shared_LimitingSubdiff
import Definitions.Def_NonconvexSplitting_Shared_StandingAssumptions
open NonconvexSplitting.Shared

open Filter Topology
open scoped InnerProductSpace

Formal statement

namespace NonconvexSplitting.ProxADMM

/-- Eq. (3) of Li–Pong (p. 3): robustness of the limiting subdifferential. -/
theorem limitingSubdiff_robust {m : ℕ} (f : EuclideanSpace ℝ (Fin m) → EReal)
    (hf : IsProperFn f) (u v : EuclideanSpace ℝ (Fin m)) (hu : f u ≠ ⊤)
    (us vs : ℕ → EuclideanSpace ℝ (Fin m))
    (hus : Tendsto us atTop (𝓝 u)) (hfus : Tendsto (fun t => f (us t)) atTop (𝓝 (f u)))
    (hvs : Tendsto vs atTop (𝓝 v)) (hmem : ∀ t, vs t ∈ LimitingSubdiff f (us t)) :
    v ∈ LimitingSubdiff f u := by sorry

end NonconvexSplitting.ProxADMM

Source

Li & Pong, Global Convergence of Splitting Methods for Nonconvex Composite Optimization, arXiv:1407.0753v6, p. 3, Eq. (3)

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph