Eq. (47): optimality condition of the proximal gradient step

Proved

NonconvexSplitting.ProxGrad.eq47_inclusion

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

nonconvex-optimizationp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1proximal-gradientvariational-analysis

Let $h$ and $P$ satisfy the standing assumptions, let $\beta > 0$ , and let $(x^t)$ be generated by the proximal gradient update (43). Then for every $t \ge 0$ ,

0 \in \nabla h(x^t) + \frac{1}{\beta}\bigl(x^{t+1} - x^t\bigr) + \partial P(x^{t+1}),

where $\partial P$ is the limiting subdifferential; that is, some $w \in \partial P(x^{t+1})$ satisfies $\nabla h(x^t) + \frac1\beta (x^{t+1} - x^t) + w = 0$ .

Passing to the limit in this inclusion along a convergent subsequence yields stationarity of cluster points.

Preamble

import Mathlib
import Definitions.Def_NonconvexSplitting_Shared_LimitingSubdiff
import Definitions.Def_NonconvexSplitting_ProxGrad_StandingAssumptions
import Definitions.Def_NonconvexSplitting_ProxGrad_IsProxGradSeq
open NonconvexSplitting.Shared

Formal statement

namespace NonconvexSplitting.ProxGrad

/-- Eq. (47) of Li–Pong (p. 19): the optimality condition of the update (43),
`0 ∈ ∇h(x^t) + (1/β)(x^{t+1} - x^t) + ∂P(x^{t+1})`, for every `t`. -/
theorem eq47_inclusion {n : ℕ} (h : EuclideanSpace ℝ (Fin n) → ℝ)
    (P : EuclideanSpace ℝ (Fin n) → EReal) (β : ℝ) (x : ℕ → EuclideanSpace ℝ (Fin n))
    (hSA : StandingAssumptions h P) (hβ : 0 < β) (hx : IsProxGradSeq h P β x) (t : ℕ) :
    ∃ w ∈ LimitingSubdiff P (x (t + 1)),
      gradient h (x t) + (1 / β) • (x (t + 1) - x t) + w = 0 := by sorry

end NonconvexSplitting.ProxGrad

Source

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

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