Prove2Me

Theorem 4: proximal gradient descends and its cluster points are stationary for β<1/ℓ\beta < 1/\ell

Proved
NonconvexSplitting.ProxGrad.theorem4

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

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

Consider min⁡xh(x)+P(x)\min_x h(x) + P(x) on Rn\mathbb{R}^n, where hh is twice continuously differentiable with a bounded Hessian and P:Rn→(−∞,+∞]P : \mathbb{R}^n \to (-\infty, +\infty] is proper and closed with well-defined proximal mappings.

Suppose there exist a twice continuously differentiable convex function qq and ℓ>0\ell > 0 such that for all xx

−ℓI⪯∇2h(x)+∇2q(x)⪯ℓI.(44)-\ell I \preceq \nabla^2 h(x) + \nabla^2 q(x) \preceq \ell I . \qquad (44)

Let (xt)(x^t) be generated by the proximal gradient update

xt+1∈Arg min⁡x{⟨∇h(xt),x−xt⟩+12β∥x−xt∥2+P(x)}(43)x^{t+1} \in \operatorname*{Arg\,min}_x \Bigl\{ \langle \nabla h(x^t), x - x^t\rangle + \frac{1}{2\beta}\|x - x^t\|^2 + P(x) \Bigr\} \qquad (43)

with β∈(0,1/ℓ)\beta \in (0, 1/\ell). Then:

  1. the algorithm is a descent algorithm: h(xt+1)+P(xt+1)≤h(xt)+P(xt)h(x^{t+1}) + P(x^{t+1}) \le h(x^t) + P(x^t) for every t≥0t \ge 0;
  2. every cluster point x∗x^* of (xt)(x^t), if one exists, is a stationary point: 0∈∇h(x∗)+∂P(x∗)0 \in \nabla h(x^*) + \partial P(x^*), with ∂\partial the limiting subdifferential.

The constant ℓ\ell bounds the curvature of hh only after its concave part is offset by the convex qq, so it may be smaller than the Lipschitz modulus of ∇h\nabla h; the result then permits step sizes beyond the classical range (0,1/L)(0, 1/L).

Formalization Note Objective values are compared in EReal. A cluster point is a limit of xφ(i)x^{\varphi(i)} for a strictly increasing φ\varphi. The start x0x^0 is arbitrary, and no boundedness of the sequence is assumed.

Preamble
import Mathlib
import Definitions.Def_NonconvexSplitting_ProxGrad_StandingAssumptions
import Definitions.Def_NonconvexSplitting_ProxGrad_HessianSandwich
import Definitions.Def_NonconvexSplitting_ProxGrad_IsProxGradSeq
import Definitions.Def_NonconvexSplitting_ProxGrad_IsStationary
open NonconvexSplitting.Shared

open Filter Topology
Formal statement
namespace NonconvexSplitting.ProxGrad

/-- Theorem 4 of Li–Pong (p. 18). Suppose `q` is twice continuously differentiable and convex,
`ℓ > 0`, and `-ℓ I ⪯ ∇²h(x) + ∇²q(x) ⪯ ℓ I` for all `x` (44). Let `{x^t}` be generated by (43)
with `β ∈ (0, 1/ℓ)`. Then the algorithm is a descent algorithm, and every cluster point of
`{x^t}` (if one exists) is a stationary point. -/
theorem theorem4 {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) :
    (∀ t, ((h (x (t + 1)) : ℝ) : EReal) + P (x (t + 1)) ≤ ((h (x t) : ℝ) : EReal) + P (x t)) ∧
    ∀ xs : EuclideanSpace ℝ (Fin n),
      (∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 xs)) → IsStationary h P xs := by sorry

end NonconvexSplitting.ProxGrad
Source
Li & Pong, Global Convergence of Splitting Methods for Nonconvex Composite Optimization, arXiv:1407.0753v6, p. 18, Theorem 4
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