§1.3, proof of Theorem 3, p. 5 — ‖x_{k+1} − x‖² ≤ ‖y_k − x‖²

Proved

NesterovFB.Weak.dist_succ_le_dist_extrap

by mikedeng1 · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

fejer-monotonicityfistaforward-backwardnesterov-accelerationp2o-batch-pfp1ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $\mathcal H$ be a real Hilbert space. Let $\Psi:\mathcal H\to\mathbb R\cup\{+\infty\}$ be proper, lower-semicontinuous and convex, and let $\Phi:\mathcal H\to\mathbb R$ be convex and continuously differentiable with $L$ -Lipschitz continuous gradient. Write $\Theta=\Psi+\Phi$ . Let $\alpha>3$ and $0<s<1/L$ , and let $(x_k)$ be a sequence generated by algorithm (2),

y_k = x_k + \frac{k-1}{k+\alpha-1}(x_k - x_{k-1}),\qquad x_{k+1} = \operatorname{prox}_{s\Psi}\big(y_k - s\nabla\Phi(y_k)\big).

Let $x^*\in\operatorname{argmin}\Theta$ . Then for every $k\ge1$ ,

\|x_{k+1}-x^*\|^2 \le \|y_k - x^*\|^2.

Each forward-backward step from the extrapolated point $y_k$ moves no farther from any minimizer. This is the first estimate of the proof of Theorem 3, from which the bound on $\delta_{k+1}-\delta_k$ follows.

Formalization Note $L\ge0$ is a nonnegative real and " $0<s<1/L$ " is written $0<s$ , $sL<1$ , which also covers $L=0$ . $\operatorname{prox}_{s\Psi}$ is given as a map $P$ satisfying the minimization property of the proximal map (it exists and is unique under the hypotheses). The run starts at $k=1$ with $x_0,x_1$ arbitrary. The hypothesis $\alpha>3$ is the standing assumption of Theorem 3; the inequality itself does not use it.

Preamble

import Mathlib
import Definitions.Def_ThreeOpSplitting_ConvexRates_Problem
import Definitions.Def_NesterovFB_Weak_Algorithm
open Filter Topology NNReal

Formal statement

namespace NesterovFB.Weak

theorem dist_succ_le_dist_extrap
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    (Ψ : H → EReal) (Φ : H → ℝ) (L : ℝ≥0) (s α : ℝ) (P : H → H) (x : ℕ → H)
    (hΨ : ThreeOpSplitting.ConvexRates.IsProperClosedConvex Ψ)
    (hΦc : ConvexOn ℝ Set.univ Φ) (hΦd : ContDiff ℝ 1 Φ)
    (hL : LipschitzWith L (gradient Φ))
    (hs : 0 < s) (hsL : s * (L : ℝ) < 1)
    (hP : ThreeOpSplitting.ConvexRates.IsProx s Ψ P)
    (hα : 3 < α)
    (hrun : NesterovFB.Rates.IsAccelFBRun Φ P α s x)
    (xstar : H) (hxstar : ∀ y, NesterovFB.Rates.theta Ψ Φ xstar ≤ NesterovFB.Rates.theta Ψ Φ y) :
    ∀ k : ℕ, 1 ≤ k → ‖x (k + 1) - xstar‖ ^ 2 ≤ ‖NesterovFB.Rates.extrap α x k - xstar‖ ^ 2 := by sorry

end NesterovFB.Weak

Source

Attouch and Peypouquet, The Rate of Convergence of Nesterov's Accelerated Forward-Backward Method is Actually Faster than 1/k^2, arXiv:1510.08740v4, p. 5, §1.3, proof of Theorem 3, display after (17) ("and so ‖x_{k+1} − x*‖² ≤ ‖y_k − x*‖²")

Human review

Endorsed by Shuze Chen · Oct 4, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 4, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

§1.3, proof of Theorem 3, p. 5 — ‖x_{k+1} − x*‖² ≤ ‖y_k − x*‖²

§1.3, proof of Theorem 3, p. 5 — ‖x_{k+1} − x‖² ≤ ‖y_k − x‖²