Prove2Me

Eq. (3.24), p. 294 — f(y_{s+1}) − f(x*) ≤ β(x_s − y_{s+1})⊤(x_s − x*) − (β/2)‖x_s − y_{s+1}‖²

Open
ConvexOptAlg.NesterovSmooth.eq_3_24

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

accelerated-gradientconvex-optimizationnesterovp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-bookp2o-v1

Let f:Rn→Rf:\mathbb R^n\to\mathbb R be convex and β\beta-smooth with β>0\beta>0, let x∗x^* be a minimizer of ff, and let (xt),(yt)(x_t),(y_t) be a run of Nesterov's accelerated gradient descent for the smooth case. Then for every s≥1s\ge1,

f(ys+1)−f(x∗)≤β(xs−ys+1)⊤(xs−x∗)−β2∥xs−ys+1∥2.f(y_{s+1})-f(x^*)\le\beta(x_s-y_{s+1})^\top(x_s-x^*)-\frac\beta2\|x_s-y_{s+1}\|^2.

This is the counterpart of (3.23) with the comparison point x∗x^* in place of ysy_s.

Formalization Note That x∗x^* is a minimizer is the book's standing assumption (p. 242); β>0\beta>0 is stated.

Preamble
import Mathlib
import Definitions.Def_ConvexOptAlg_NesterovSmooth_Defs
open scoped InnerProductSpace
Formal statement
namespace ConvexOptAlg.NesterovSmooth

/-- Eq. (3.24) (Bubeck, arXiv:1405.4980v2, proof of Theorem 3.19, p. 294): along a run of
Nesterov's accelerated gradient descent on a convex β-smooth `f` with minimizer `x*`, for every
`s ≥ 1`, `f(y_{s+1}) − f(x*) ≤ β(x_s − y_{s+1})⊤(x_s − x*) − (β/2)‖x_s − y_{s+1}‖²`. -/
theorem eq_3_24 {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ)
    (g : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) (β : ℝ) (hβ : 0 < β)
    (hconv : ConvexOn ℝ Set.univ f) (hf : IsBetaSmooth f g β)
    (xstar : EuclideanSpace ℝ (Fin n)) (hmin : ∀ z, f xstar ≤ f z)
    (x y : ℕ → EuclideanSpace ℝ (Fin n)) (hrun : IsNesterovRun g β x y) (s : ℕ) (hs : 1 ≤ s) :
    f (y (s + 1)) - f xstar ≤
      β * ⟪x s - y (s + 1), x s - xstar⟫_ℝ - β / 2 * ‖x s - y (s + 1)‖ ^ 2 := by sorry

end ConvexOptAlg.NesterovSmooth
Source
Bubeck, arXiv:1405.4980v2, proof of Theorem 3.19, Eq. (3.24), p. 294

View graph