Eq. (46): sufficient decrease of the proximal gradient method

Proved

NonconvexSplitting.ProxGrad.eq46_sufficient_decrease

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

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

Let $h$ and $P$ satisfy the standing assumptions ( $h$ is $C^2$ with bounded Hessian; $P$ is proper, closed, with well-defined proximal mappings). Let $q : \mathbb{R}^n \to \mathbb{R}$ be twice continuously differentiable and convex, $\ell > 0$ , and suppose $-\ell I \preceq \nabla^2 h(x) + \nabla^2 q(x) \preceq \ell I$ for all $x$ . Let $\beta > 0$ and let $(x^t)$ be generated by the proximal gradient update (43). Then for every $t \ge 0$ ,

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

When $\beta < 1/\ell$ the coefficient is negative, so the objective decreases along the iterates by a multiple of the squared step length.

Formalization Note Both sides are in EReal; when $P(x^t) = +\infty$ the right side is $+\infty$ . Only $\beta > 0$ is assumed, as the inequality itself does not need $\beta < 1/\ell$ .

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

/-- Eq. (46) of Li–Pong (p. 18), first and last members:
`h(x^{t+1}) + P(x^{t+1}) ≤ h(x^t) + P(x^t) + (ℓ/2 - 1/(2β)) ‖x^{t+1} - x^t‖²`, in `EReal`. -/
theorem eq46_sufficient_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) (t : ℕ) :
    ((h (x (t + 1)) : ℝ) : EReal) + P (x (t + 1)) ≤
      ((h (x t) : ℝ) : EReal) + P (x t) +
        (((ℓ / 2 - 1 / (2 * β)) * ‖x (t + 1) - x t‖ ^ 2 : ℝ) : EReal) := by sorry

end NonconvexSplitting.ProxGrad

Source

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

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