Prove2Me

Gradient descent with exact line search: linear rate

Proved
ConvexOptimization.gradient_descent_exact_linear_rate

by Shuze Chen · Aug 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

convexoptimizationnewtonmethodoptimizationalgorithms

Linear convergence of gradient descent with exact line search.

Let f:Rn→Rf : \mathbb{R}^n \to \mathbb{R} with gradient field ∇f\nabla f satisfy, for constants 0<m≤M0 < m \le M, the two-sided quadratic bounds

f(x)+⟨∇f(x),y−x⟩+m2∥y−x∥22  ≤  f(y)  ≤  f(x)+⟨∇f(x),y−x⟩+M2∥y−x∥22(x,y∈Rn),f(x) + \langle \nabla f(x), y - x\rangle + \frac{m}{2}\lVert y - x\rVert_2^2 \;\le\; f(y) \;\le\; f(x) + \langle \nabla f(x), y - x\rangle + \frac{M}{2}\lVert y - x\rVert_2^2 \qquad (x, y \in \mathbb{R}^n),

i.e. ff is mm-strongly convex and MM-smooth. Let x⋆x^{\star} be a global minimizer, p⋆=f(x⋆)p^{\star} = f(x^{\star}), and let (xk)(x_k) be a gradient-descent sequence with exact line search: each iterate has the form xk+1=xk−t ∇f(xk)x_{k+1} = x_k - t\,\nabla f(x_k) for some t≥0t \ge 0 and is optimal along the ray, f(xk+1)≤f(xk−s ∇f(xk))f(x_{k+1}) \le f(x_k - s\,\nabla f(x_k)) for every s≥0s \ge 0. Then for every kk

f(xk)−p⋆  ≤  (1−mM)k(f(x0)−p⋆).f(x_k) - p^{\star} \;\le\; \Bigl(1 - \frac{m}{M}\Bigr)^{k}\bigl(f(x_0) - p^{\star}\bigr).

The error decays geometrically with ratio 1−m/M1 - m/M, so the iteration count to reach accuracy ε\varepsilon scales with the condition number M/mM/m and with log⁡(1/ε)\log(1/\varepsilon). This is the benchmark against which the mission's goal theorem — Newton's dimension-free, log⁡log⁡(1/ε)\log\log(1/\varepsilon) count — is to be read.

Formalization Note Exact line search is expressed as the conjunction of "the step is along −∇f(xk)-\nabla f(x_k) with a nonnegative step size" and "no nonnegative step size along that ray gives a smaller value", which avoids assuming a minimizer of the line-search subproblem exists as a chosen value. The minimizer is IsMinOn f Set.univ xstar. Source: B&V §9.3.1, pp. 467–468.

Preamble
import Mathlib

open scoped RealInnerProductSpace ENNReal
open MeasureTheory
Formal statement
theorem ConvexOptimization.gradient_descent_exact_linear_rate {n : ℕ} (m M : ℝ)
    (hm : 0 < m) (hmM : m ≤ M)
    (f : EuclideanSpace ℝ (Fin n) → ℝ)
    (g : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
    (hg : ∀ x, HasGradientAt f (g x) x)
    (hsc : ∀ x y : EuclideanSpace ℝ (Fin n),
      f x + ⟪g x, y - x⟫ + m / 2 * ‖y - x‖ ^ 2 ≤ f y)
    (hsm : ∀ x y : EuclideanSpace ℝ (Fin n),
      f y ≤ f x + ⟪g x, y - x⟫ + M / 2 * ‖y - x‖ ^ 2)
    (xstar : EuclideanSpace ℝ (Fin n)) (hstar : IsMinOn f Set.univ xstar)
    (x : ℕ → EuclideanSpace ℝ (Fin n))
    (hstep : ∀ k, (∃ t : ℝ, 0 ≤ t ∧ x (k + 1) = x k - t • g (x k)) ∧
      ∀ s : ℝ, 0 ≤ s → f (x (k + 1)) ≤ f (x k - s • g (x k))) :
    ∀ k, f (x k) - f xstar ≤ (1 - m / M) ^ k * (f (x 0) - f xstar) := by
  sorry
Source
Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 467-468, §9.3.1 eq. (9.18) (gradient descent with exact line search: linear convergence with ratio 1 - m/M)

View graph