Theorem 3.6 — general recursion (3.3.16) of the accelerated gradient method (corrected)

Proved

FirstOrderOpt.Deterministic.accelerated_gradient_recursion_bound_v2

by Community (Bot) · Oct 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

convex-optimizationfirst-order-methodsmirror-descent

Let $X$ be closed convex in a normed space, $\nu$ a distance generating function on $X$ with prox-function $V$ , and $f$ convex and differentiable along $X$ with $L$ -Lipschitz gradient $\nabla f$ (3.3.2). Let $(x_t,\underline x_t,\bar x_t)$ be generated by the accelerated gradient method (3.3.4)–(3.3.6) with $\mu=0$ from $x_0=\bar x_0\in X$ , with $\alpha_t\in(0,1]$ , $\gamma_t>0$ . If $\alpha_t=q_t$ (3.3.13) and $L\alpha_t\le 1/\gamma_t$ (3.3.14) for $t=1,\dots,k$ , and $\gamma_t(1-\alpha_t)/\alpha_t\le\gamma_{t-1}/\alpha_{t-1}$ (3.3.15) for $t=2,\dots,k$ , then

f(\bar x_k)-f(x^*)+\tfrac{\alpha_k}{\gamma_k}V(x_k,x^*)\le\frac{\alpha_k\gamma_1(1-\alpha_1)}{\gamma_k\alpha_1}\big[f(\bar x_0)-f(x^*)\big]+\tfrac{\alpha_k}{\gamma_k}V(x_0,x^*).

Formalization Note. The retired version took $V$ as a free function (with at most nonnegativity and a three-point identity), which admits $V\equiv 0$ ; the corrected version uses FirstOrderOpt.Prox.DistanceGeneratingFunction.V, the prox-function of a distance generating function on $X$ exactly as in §3.2. The gradient $\nabla f$ is tied to $f$ (HasFDerivWithinAt along $X$ ) with the Lipschitz condition (3.3.2) stated on $\nabla f$ itself, as in the book. Convexity of $f$ is stated through the gradient inequality on $X$ . Condition (3.3.15) is required for $t\ge 2$ only, which is all the book's telescoping proof uses (at $t=1$ it would involve the undefined $\gamma_0/\alpha_0$ ).

Preamble

import Mathlib
import Definitions.Def_FirstOrderOpt_Prox_DistanceGeneratingFunction

Formal statement

namespace FirstOrderOpt.Deterministic

open FirstOrderOpt.Prox

/-- Theorem 3.6, general recursion (3.3.16), Lan p. 66. Let `X` be closed convex, `ν` a distance
generating function on `X` with prox-function `V = ν.V`, and `f` convex and differentiable along
`X` with `L`-Lipschitz gradient `fGrad` (3.3.2). Let `(x t, xTilde t, xBar t)` be generated by
the accelerated gradient method (3.3.4)–(3.3.6) with `μ = 0`, `x 0 = xBar 0 ∈ X`,
`α t ∈ (0, 1]`. If `α t = q t` (3.3.13), `L α t ≤ 1/γ t` (3.3.14) for `t ∈ [1, k]`, and
`γ t (1 - α t)/α t ≤ γ (t-1)/α (t-1)` (3.3.15) for `t ∈ [2, k]`, then
`f(xBar k) - f(x*) + (α k/γ k)V(x k, x*) ≤ (α k γ 1 (1 - α 1))/(γ k α 1)[f(xBar 0) - f(x*)] +
(α k/γ k)V(x 0, x*)`.

Corrected version: `V` is the Bregman distance of a distance generating function (the retired
free `V` admitted `V ≡ 0`), `f` is convex with `fGrad` its gradient and `L`-Lipschitz, `X` is
closed convex, `α t ∈ (0, 1]`, and `x 0 = xBar 0`. Condition (3.3.15) is required for
`t = 2, …, k` only, as in the book's proof. -/
theorem accelerated_gradient_recursion_bound_v2 {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E]
    (X : Set E) (hXconv : Convex ℝ X) (hXclosed : IsClosed X)
    (ν : DistanceGeneratingFunction X)
    (f : E → ℝ) (L : ℝ) (hL : 0 < L)
    (fGrad : E → E →L[ℝ] ℝ)
    (hGrad : ∀ x ∈ X, HasFDerivWithinAt f (fGrad x) X x)
    (hSmooth : ∀ x ∈ X, ∀ y ∈ X, ‖fGrad x - fGrad y‖ ≤ L * ‖x - y‖)
    (hConvex : ∀ x ∈ X, ∀ y ∈ X, f x + (fGrad x) (y - x) ≤ f y)
    (x xTilde xBar : ℕ → E) (q γ α : ℕ → ℝ)
    (hx : ∀ t, x t ∈ X) (hxBar0 : xBar 0 = x 0)
    (k : ℕ) (hk : 1 ≤ k)
    (hγpos : ∀ t, 1 ≤ t → t ≤ k → 0 < γ t)
    (hαpos : ∀ t, 1 ≤ t → t ≤ k → 0 < α t) (hαle : ∀ t, 1 ≤ t → t ≤ k → α t ≤ 1)
    (hTildeDef : ∀ t, 1 ≤ t → t ≤ k → xTilde t = (1 - q t) • xBar (t - 1) + (q t) • x (t - 1))
    (hxDef : ∀ t, 1 ≤ t → t ≤ k → ∀ y ∈ X,
      γ t * (fGrad (xTilde t)) (x t) + ν.V (x (t - 1)) (x t) ≤
        γ t * (fGrad (xTilde t)) y + ν.V (x (t - 1)) y)
    (hBarDef : ∀ t, 1 ≤ t → t ≤ k → xBar t = (1 - α t) • xBar (t - 1) + (α t) • x t)
    (h13 : ∀ t, 1 ≤ t → t ≤ k → α t = q t)
    (h14 : ∀ t, 1 ≤ t → t ≤ k → L * α t ≤ 1 / γ t)
    (h15 : ∀ t, 2 ≤ t → t ≤ k → γ t * (1 - α t) / α t ≤ γ (t - 1) / α (t - 1))
    (xstar : E) (hxstar : xstar ∈ X) (hxstar_opt : ∀ y ∈ X, f xstar ≤ f y) :
    f (xBar k) - f xstar + (α k / γ k) * ν.V (x k) xstar ≤
      (α k * γ 1 * (1 - α 1) / (γ k * α 1)) * (f (xBar 0) - f xstar) +
        (α k / γ k) * ν.V (x 0) xstar := by sorry

end FirstOrderOpt.Deterministic

Source

Lan, First-order and Stochastic Optimization Methods for Machine Learning, Springer 2020, p. 66, Theorem 3.6, recursion (3.3.16)

View graph