Prove2Me

Theorem 1, p. 13 — for f ∈ S²_{μ,L} and 0 < s ≤ 1/L, the NAG-SC high-resolution ODE satisfies f(X(t)) − f(x⋆) ≤ (2‖x₀ − x⋆‖²/s) e^{−√μ t/4}

Proved
HighResODE.NAGSCODE.theorem_1

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

accelerated-gradienthigh-resolution-odelinear-convergencenesterovp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1strongly-convex

Let f∈Sμ,L2(Rn)f\in\mathcal S^2_{\mu,L}(\mathbb R^n), that is, ff is LL-smooth, μ\mu-strongly convex with 0<μ≤L0<\mu\le L, of class C2C^2 with a Lipschitz-continuous Hessian, and let x⋆x^\star be its minimizer. Let 0<s≤1/L0<s\le1/L be a step size and x0∈Rnx_0\in\mathbb R^n. Let X=X(t)X=X(t) be the solution of the high-resolution ODE of NAG-SC,

X¨(t)+2μ X˙(t)+s ∇2f(X(t))X˙(t)+(1+μs)∇f(X(t))=0,X(0)=x0, X˙(0)=−2s ∇f(x0)1+μs.\ddot X(t)+2\sqrt\mu\,\dot X(t)+\sqrt s\,\nabla^2 f(X(t))\dot X(t)+\big(1+\sqrt{\mu s}\big)\nabla f(X(t))=0,\qquad X(0)=x_0,\ \dot X(0)=-\frac{2\sqrt s\,\nabla f(x_0)}{1+\sqrt{\mu s}}.

Then for every t≥0t\ge0,

f(X(t))−f(x⋆)≤2∥x0−x⋆∥2s e−μt4.f(X(t))-f(x^\star)\le\frac{2\|x_0-x^\star\|^2}{s}\,e^{-\frac{\sqrt\mu t}{4}}.

The function value along the high-resolution ODE of Nesterov's accelerated gradient method for strongly convex functions converges linearly, at the accelerated rate μ\sqrt\mu rather than μ\mu; with s=1/Ls=1/L the bound reads f(X)−f(x⋆)≤2L∥x0−x⋆∥2e−μt/4f(X)-f(x^\star)\le2L\|x_0-x^\star\|^2e^{-\sqrt\mu t/4}. It is the continuous-time counterpart of the discrete rate for NAG-SC in Theorem 3 of the same paper.

Formalization Note. A solution is any pair of curves (X,V)(X,V) with VV the one-sided derivative of XX on [0,∞)[0,\infty), VV having the derivative the ODE prescribes, and the initial conditions above; existence and uniqueness (Proposition 2.1) are not assumed, so "the solution" is read as "every solution". The minimizer x⋆x^\star is a point with f(x⋆)≤f(z)f(x^\star)\le f(z) for all zz. ∇2f(X)X˙\nabla^2 f(X)\dot X is the Fréchet derivative of ∇f\nabla f at XX applied to X˙\dot X. The Hessian's Lipschitz constant is not fixed.

Preamble
import Mathlib
import Definitions.Def_HighResODE_NAGSCODE_Setting

open scoped InnerProductSpace
Formal statement
namespace HighResODE.NAGSCODE

theorem theorem_1 {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ) (μ L s : ℝ) (hf : IsS2 f μ L)
    (xs : EuclideanSpace ℝ (Fin n)) (hmin : ∀ z, f xs ≤ f z) (hs : 0 < s) (hsL : s ≤ 1 / L)
    (x0 : EuclideanSpace ℝ (Fin n)) (X V : ℝ → EuclideanSpace ℝ (Fin n))
    (hsol : IsNAGSCODE f μ s x0 X V) :
    ∀ t, 0 ≤ t →
      f (X t) - f xs ≤ 2 * ‖x0 - xs‖ ^ 2 / s * Real.exp (-(Real.sqrt μ * t / 4)) := by sorry

end HighResODE.NAGSCODE
Source
Shi, Du, Jordan & Su, Understanding the Acceleration Phenomenon via High-Resolution Differential Equations, arXiv:1810.08907v3, p. 13, Theorem 1
Human review

  • Endorsed by Shuze Chen · Oct 10, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 10, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph