Proof of Theorem 3.19, p. 294 — the step sequence satisfies λ²_{s−1} = λ²_s − λ_s

Open

ConvexOptAlg.NesterovSmooth.lam_sq_identity

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

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

Let $\lambda_0=0$ and $\lambda_t=\frac{1+\sqrt{1+4\lambda_{t-1}^2}}2$ for $t\ge1$ . Then for every $s\ge1$ ,

\lambda_{s-1}^2=\lambda_s^2-\lambda_s.

The book uses this identity "by definition" to turn the one-step inequality into a telescoping one.

Preamble

import Mathlib
import Definitions.Def_ConvexOptAlg_NesterovSmooth_Defs
open scoped InnerProductSpace

Formal statement

namespace ConvexOptAlg.NesterovSmooth

/-- The identity `λ_{s−1}² = λ_s² − λ_s` used in the proof of Theorem 3.19 (Bubeck,
arXiv:1405.4980v2, p. 294, "by definition"), for every `s ≥ 1`. -/
theorem lam_sq_identity (s : ℕ) (hs : 1 ≤ s) :
    lam (s - 1) ^ 2 = lam s ^ 2 - lam s := by sorry

end ConvexOptAlg.NesterovSmooth

Source

Bubeck, arXiv:1405.4980v2, proof of Theorem 3.19, p. 294 ("using that by definition λ²_{s−1} = λ²_s − λ_s")

View graph