Prove2Me

Eq. (3.20), p. 292 — Φ*_{s+1} ≥ (1 − 1/√κ)Φ*_s + (1 − 1/√κ)∇f(x_s)⊤(x_s − y_s) + f(x_s)/√κ − ‖∇f(x_s)‖²/(2β)

Open
ConvexOptAlg.NesterovStrong.eq_3_20

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

accelerated-gradientconvex-optimizationestimate-sequencep2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-bookp2o-v1

Let f:Rn→Rf:\mathbb R^n\to\mathbb R be α\alpha-strongly convex and β\beta-smooth with α,β>0\alpha,\beta>0, κ=β/α\kappa=\beta/\alpha, let (xt),(yt)(x_t),(y_t) be a run of Nesterov's accelerated gradient descent, and let Φs∗=Φs(vs)=min⁡Φs\Phi^*_s=\Phi_s(v_s)=\min\Phi_s with Φs\Phi_s, vsv_s as in (3.17), (3.21). Then for every s≥1s\ge1,

Φs+1∗≥(1−1κ)Φs∗+(1−1κ)∇f(xs)⊤(xs−ys)+1κf(xs)−12β∥∇f(xs)∥2.\Phi^*_{s+1}\ge\Big(1-\frac1{\sqrt\kappa}\Big)\Phi^*_s+\Big(1-\frac1{\sqrt\kappa}\Big)\nabla f(x_s)^\top(x_s-y_s)+\frac1{\sqrt\kappa}f(x_s)-\frac1{2\beta}\|\nabla f(x_s)\|^2 .

This is the inductive step of (3.19): its right-hand side is an upper bound on f(ys+1)f(y_{s+1}) obtained from smoothness, convexity and the induction hypothesis.

Formalization Note Φs∗\Phi^*_s is the value of Φs\Phi_s at vsv_s, which equals the book's min⁡Φs\min\Phi_s by eq_3_21_form.

Preamble
import Mathlib
import Definitions.Def_OnlineConvexOpt_ConvexBasics_StronglyConvexOn
import Definitions.Def_ConvexOptAlg_NesterovStrong_Defs

open scoped InnerProductSpace
Formal statement
namespace ConvexOptAlg.NesterovStrong

/-- Bubeck, proof of Theorem 3.18, Eq. (3.20), p. 292: for a `β`-smooth, `α`-strongly convex
`f` on `ℝⁿ` and a run `(x, y)` of Nesterov's accelerated gradient descent, for every `s ≥ 1`,
`Φ∗_{s+1} ≥ (1 − 1/√κ)Φ∗_s + (1 − 1/√κ)∇f(x_s)ᵀ(x_s − y_s) + (1/√κ) f(x_s) − (1/(2β))‖∇f(x_s)‖²`. -/
theorem eq_3_20 {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ)
    (g : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) (α β : ℝ)
    (hα : 0 < α) (hβ : 0 < β)
    (hsc : OnlineConvexOpt.ConvexBasics.StronglyConvexOn Set.univ f g α)
    (hsm : IsBetaSmooth f g β)
    (x y : ℕ → EuclideanSpace ℝ (Fin n)) (hrun : IsNesterovSCRun g α β x y)
    (s : ℕ) (hs : 1 ≤ s) :
    PhiStar f g α β x (s + 1) ≥
      (1 - 1 / Real.sqrt (kappa α β)) * PhiStar f g α β x s +
        (1 - 1 / Real.sqrt (kappa α β)) * ⟪g (x s), x s - y s⟫_ℝ +
          1 / Real.sqrt (kappa α β) * f (x s) - 1 / (2 * β) * ‖g (x s)‖ ^ 2 := by sorry

end ConvexOptAlg.NesterovStrong
Source
Bubeck, arXiv:1405.4980v2, proof of Theorem 3.18, Eq. (3.20), p. 292

View graph