Prove2Me

Eq. (3.22), p. 292 — Φ*_{s+1} + (α/2)‖x_s − v_{s+1}‖² = (1 − 1/√κ)Φ*_s + (α/2)(1 − 1/√κ)‖x_s − v_s‖² + f(x_s)/√κ

Open
ConvexOptAlg.NesterovStrong.eq_3_22

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

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

Let α>0\alpha>0, β∈R\beta\in\mathbb R, κ=β/α\kappa=\beta/\alpha, let ff, gg (in the role of ∇f\nabla f) and the points (xs)s≥1(x_s)_{s\ge1} be arbitrary, and let Φs\Phi_s, vsv_s and Φs∗=Φs(vs)\Phi^*_s=\Phi_s(v_s) be as in (3.17) and (3.21). Then for every s≥1s\ge1,

Φs+1∗+α2∥xs−vs+1∥2=(1−1κ)Φs∗+α2(1−1κ)∥xs−vs∥2+1κf(xs).\Phi^*_{s+1}+\frac\alpha2\|x_s-v_{s+1}\|^2=\Big(1-\frac1{\sqrt\kappa}\Big)\Phi^*_s+\frac\alpha2\Big(1-\frac1{\sqrt\kappa}\Big)\|x_s-v_s\|^2+\frac1{\sqrt\kappa}f(x_s).

This identity, obtained by evaluating Φs+1\Phi_{s+1} at xsx_s, gives a closed recursion for the minimum values Φs∗\Phi^*_s.

Formalization Note Like eq_3_21_form, the identity is algebraic and is stated for any sequence of points and any map gg.

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.22), p. 292: for any `α > 0`, any `f`, gradient map
`g`, `β`, any sequence of points `x_s` and every `s ≥ 1`,
`Φ∗_{s+1} + (α/2)‖x_s − v_{s+1}‖² = (1 − 1/√κ)Φ∗_s + (α/2)(1 − 1/√κ)‖x_s − v_s‖² + (1/√κ) f(x_s)`. -/
theorem eq_3_22 {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ)
    (g : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) (α β : ℝ)
    (hα : 0 < α) (x : ℕ → EuclideanSpace ℝ (Fin n))
    (s : ℕ) (hs : 1 ≤ s) :
    PhiStar f g α β x (s + 1) + α / 2 * ‖x s - v g α β x (s + 1)‖ ^ 2 =
      (1 - 1 / Real.sqrt (kappa α β)) * PhiStar f g α β x s +
        α / 2 * (1 - 1 / Real.sqrt (kappa α β)) * ‖x s - v g α β x s‖ ^ 2 +
          1 / Real.sqrt (kappa α β) * f (x s) := by sorry

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

View graph