Successive differences vanish when a cluster point exists

Proved

NonconvexSplitting.ProxGrad.succ_diff_tendsto_zero

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

nonconvex-optimizationp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1proximal-gradient

Assume the hypotheses of Theorem 4: the standing assumptions on $h$ and $P$ ; $q$ twice continuously differentiable and convex; $\ell > 0$ with $-\ell I \preceq \nabla^2 h(x) + \nabla^2 q(x) \preceq \ell I$ for all $x$ ; step size $\beta \in (0, 1/\ell)$ ; and $(x^t)$ generated by the proximal gradient update (43). If $(x^t)$ has a cluster point, then

\lim_{t \to \infty} \|x^{t+1} - x^t\| = 0 .

This is the step that lets the iterate $x^{t_i+1}$ inherit the limit of a convergent subsequence $x^{t_i}$ .

Formalization Note A cluster point is a limit of $x^{\varphi(i)}$ for some strictly increasing $\varphi : \mathbb{N} \to \mathbb{N}$ . No finiteness of $P(x^0)$ is assumed.

Preamble

import Mathlib
import Definitions.Def_NonconvexSplitting_ProxGrad_StandingAssumptions
import Definitions.Def_NonconvexSplitting_ProxGrad_HessianSandwich
import Definitions.Def_NonconvexSplitting_ProxGrad_IsProxGradSeq

open Filter Topology

Formal statement

namespace NonconvexSplitting.ProxGrad

/-- Li–Pong (p. 19): under the hypotheses of Theorem 4, if `{x^t}` has a cluster point then
`‖x^{t+1} - x^t‖ → 0`. -/
theorem succ_diff_tendsto_zero {n : ℕ} (h q : EuclideanSpace ℝ (Fin n) → ℝ) (P : EuclideanSpace ℝ (Fin n) → EReal) (ℓ β : ℝ)
    (x : ℕ → EuclideanSpace ℝ (Fin n))
    (hSA : StandingAssumptions h P) (hq : ContDiff ℝ 2 q) (hq_convex : ConvexOn ℝ Set.univ q)
    (hℓ : 0 < ℓ) (h44 : HessianSandwich h q ℓ) (hβ : 0 < β)
    (hβℓ : β < 1 / ℓ) (hx : IsProxGradSeq h P β x)
    (hclu : ∃ xs : EuclideanSpace ℝ (Fin n), ∃ φ : ℕ → ℕ,
      StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 xs)) :
    Tendsto (fun t => ‖x (t + 1) - x t‖) atTop (𝓝 0) := by sorry

end NonconvexSplitting.ProxGrad

Source

Li & Pong, Global Convergence of Splitting Methods for Nonconvex Composite Optimization, arXiv:1407.0753v6, p. 19, first paragraph of the page

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