Theorem 6, p. 13 — the generalized Nesterov scheme with r > 3 has f(x_k) − f⋆ ≤ (r − 1)²‖x₀ − x⋆‖²/(2s(k + r − 2)²)

Proved

NesterovODE.GenScheme.theorem_6

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

accelerated-gradientconvergence-ratenesterov-odep2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1proximal-gradient

Let $\mathcal H$ be a real Hilbert space. Minimize $f=g+h$ , where $g:\mathcal H\to\mathbb R$ is convex and continuously differentiable with $L$ -Lipschitz gradient for some $L>0$ (that is, $g\in\mathcal F_L$ ), and $h:\mathcal H\to\mathbb R\cup\{+\infty\}$ is proper, lower semicontinuous and convex. Assume $f$ has a minimizer $x^\star$ and write $f^\star=f(x^\star)$ . Let $r>3$ and $0<s\le1/L$ , and let $(x_k)$ be generated by the generalized Nesterov scheme

x_k=y_{k-1}-sG_s(y_{k-1}),\qquad y_k=x_k+\frac{k-1}{k+r-1}(x_k-x_{k-1}),\qquad y_0=x_0,

where $G_s(y)=\big(y-\operatorname{prox}_{sh}(y-s\nabla g(y))\big)/s$ is the proximal subgradient. Then for every $k\ge1$ ,

f(x_k)-f^\star\le\frac{(r-1)^2\|x_0-x^\star\|^2}{2s(k+r-2)^2},

and

\sum_{k=1}^{\infty}(k+r-1)\big(f(x_k)-f^\star\big)\le\frac{(r-1)^2\|x_0-x^\star\|^2}{2s(r-3)} .

The first bound shows that replacing the constant $3$ in Nesterov's momentum coefficient $(k-1)/(k+2)$ by any $r>3$ keeps the $O(1/k^2)$ rate; the second, which does not follow from the first, shows the gap is summable against weights of order $k$ , so it cannot stay of order $1/k^2$ along a set of indices of positive density.

Formalization Note. The proximal map $\operatorname{prox}_{sh}$ is any $P$ with IsProx s h P; $h$ is assumed lower semicontinuous (closed) in addition to the paper's "convex, possibly assuming the value $\infty$ ", because that is what makes the $\operatorname{argmin}$ in $G_s$ exist. $r>3$ is the standing assumption of §4.1, which the theorem does not restate. $s\le1/L$ is written $sL\le1$ . The run includes the first step $x_1=P(x_0-s\nabla g(x_0))$ . Values of $f$ lie in EReal. The first bound is claimed for $k\ge1$ ( $x_0$ may lie outside the domain of $h$ ). The infinite series of nonnegative terms is stated through all its partial sums $\sum_{k=1}^K$ , which is equivalent and avoids the junk value of an unconditional tsum.

Preamble

import Mathlib
import Definitions.Def_ThreeOpSplitting_ConvexRates_Problem
import Definitions.Def_NesterovFB_Rates_Algorithm
import Definitions.Def_NesterovODE_GenScheme_Run

open InnerProductSpace NesterovFB.Rates ThreeOpSplitting.ConvexRates

Formal statement

namespace NesterovODE.GenScheme

theorem theorem_6 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    (Ψ : H → EReal) (Φ : H → ℝ) (L : NNReal) (s r : ℝ) (P : H → H) (x : ℕ → H) (xstar : H)
    (hΨ : IsProperClosedConvex Ψ)
    (hΦc : ConvexOn ℝ Set.univ Φ) (hΦd : ContDiff ℝ 1 Φ)
    (hL0 : 0 < L) (hL : LipschitzWith L (gradient Φ))
    (hs : 0 < s) (hsL : s * L ≤ 1)
    (hP : IsProx s Ψ P)
    (hr : 3 < r)
    (hrun : IsGenNesterovRun Φ P r s x)
    (hmin : ∀ y : H, theta Ψ Φ xstar ≤ theta Ψ Φ y) :
    (∀ k : ℕ, 1 ≤ k →
      theta Ψ Φ (x k) - theta Ψ Φ xstar
        ≤ (((r - 1) ^ 2 * ‖x 0 - xstar‖ ^ 2 / (2 * s * ((k : ℝ) + r - 2) ^ 2) : ℝ) : EReal)) ∧
    (∀ K : ℕ,
      ∑ k ∈ Finset.Icc 1 K, (((k : ℝ) + r - 1 : ℝ) : EReal) * (theta Ψ Φ (x k) - theta Ψ Φ xstar)
        ≤ (((r - 1) ^ 2 * ‖x 0 - xstar‖ ^ 2 / (2 * s * (r - 3)) : ℝ) : EReal)) := by sorry

end NesterovODE.GenScheme

Source

Su, Boyd, Candès, A Differential Equation for Modeling Nesterov's Accelerated Gradient Method, arXiv:1503.01243v2, p. 13, Theorem 6 (setting on p. 13; r > 3 from §4.1, p. 12)

Human review

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

View graph