Summed decrease bound after (46)

Proved

NonconvexSplitting.ProxGrad.summed_decrease

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

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

Under the hypotheses of (46) (standing assumptions on $h$ and $P$ ; $q$ convex and $C^2$ ; $\ell > 0$ with $-\ell I \preceq \nabla^2 h + \nabla^2 q \preceq \ell I$ ; $\beta > 0$ ; $(x^t)$ generated by (43)), for every $N$ with $N - 1 > 0$ ,

\Bigl(\frac{1}{2\beta} - \frac{\ell}{2}\Bigr)\sum_{t=0}^{N-1}\|x^{t+1} - x^t\|^2 + h(x^N) + P(x^N) \le h(x^0) + P(x^0).

Equivalently, where $P(x^N)$ is finite (which is the case for $N \ge 1$ , as $x^N$ minimizes a proper function), $\bigl(\frac{1}{2\beta} - \frac{\ell}{2}\bigr)\sum_{t=0}^{N-1}\|x^{t+1}-x^t\|^2 \le h(x^0) + P(x^0) - h(x^N) - P(x^N)$ , the form printed in the paper.

Formalization Note The additive form avoids the undefined difference $+\infty - (+\infty)$ in EReal. The range $N \ge 2$ is the paper's "any $N - 1 > 0$ ".

Preamble

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

Formal statement

namespace NonconvexSplitting.ProxGrad

/-- The display after (46) in Li–Pong (p. 18), in additive form: for `N - 1 > 0`,
`(1/(2β) - ℓ/2) Σ_{t=0}^{N-1} ‖x^{t+1} - x^t‖² + h(x^N) + P(x^N) ≤ h(x^0) + P(x^0)`, in `EReal`. -/
theorem summed_decrease {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 < β)
    (hx : IsProxGradSeq h P β x) (N : ℕ) (hN : 1 < N) :
    (((1 / (2 * β) - ℓ / 2) * ∑ t ∈ Finset.range N, ‖x (t + 1) - x t‖ ^ 2 : ℝ) : EReal) +
        ((h (x N) : ℝ) : EReal) + P (x N) ≤
      ((h (x 0) : ℝ) : EReal) + P (x 0) := by sorry

end NonconvexSplitting.ProxGrad

Source

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

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