Prove2Me

Gradient descent with exact line search: linear rate

Proved
ConvexOptimization.gradient_descent_exact_linear_rate

by Shuze Chen · Aug 13, 2026 · Mathlib c5ea003 (Lean v4.30.0)

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)
Read-back

What the Lean code literally says, in plain math · claude-fable-5

For every n∈Nn \in \mathbb{N} (including 00) and reals m,Mm, M with 0<m0 < m and m≤Mm \le M (hence 0<M0 < M and 0≤1−m/M<10 \le 1 - m/M < 1), given: f:Rn→Rf : \mathbb{R}^n \to \mathbb{R} with gradient field gg (for every xx, g(x)g(x) is the gradient of ff at xx); the strong-convexity inequality f(x)+⟨g(x),y−x⟩+m2∥y−x∥2≤f(y)f(x) + \langle g(x), y-x \rangle + \tfrac{m}{2}\lVert y-x \rVert^2 \le f(y) for all x,yx, y; the smoothness upper bound f(y)≤f(x)+⟨g(x),y−x⟩+M2∥y−x∥2f(y) \le f(x) + \langle g(x), y-x \rangle + \tfrac{M}{2}\lVert y-x \rVert^2 for all x,yx, y; a point x\*x^\* that globally minimizes ff over the whole space (f(x\*)≤f(y)f(x^\*) \le f(y) for all yy); and a sequence x:N→Rnx : \mathbb{N} \to \mathbb{R}^n such that for every kk both: (a) there exists a real t≥0t \ge 0 with xk+1=xk−t g(xk)x_{k+1} = x_k - t\, g(x_k) (the next iterate lies on the negative-gradient ray; tt is not required to be a minimizing step, and t=0t = 0 is allowed), and (b) for every real s≥0s \ge 0, f(xk+1)≤f(xk−s g(xk))f(x_{k+1}) \le f(x_k - s\, g(x_k)) (the next iterate is at least as good as every point of the ray with nonnegative step — an exact-line-search condition); then the conclusion is: for every k∈Nk \in \mathbb{N},

f(xk)−f(x\*)≤(1−mM)k(f(x0)−f(x\*)).f(x_k) - f(x^\*) \le \Big(1 - \frac{m}{M}\Big)^{k} \big(f(x_0) - f(x^\*)\big).

At k=0k = 0 this is an equality-as-inequality (the factor is 11). The initial point x0x_0 is unconstrained.

Human review

  • Endorsed by Community (Bot) · Aug 13, 2026

  • Endorsed by Shuze Chen · Aug 13, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph