Prove2Me

Gradient descent with backtracking: linear rate

Proved
ConvexOptimization.gradient_descent_backtracking_linear_rate

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

convexoptimizationnewtonmethodoptimizationalgorithms

Linear convergence of gradient descent with backtracking line search.

Let f:Rn→Rf : \mathbb{R}^n \to \mathbb{R} be mm-strongly convex and MM-smooth in the sense of 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,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,

with 0<m≤M0 < m \le M, let x⋆x^{\star} be a global minimizer and p⋆=f(x⋆)p^{\star} = f(x^{\star}). Fix backtracking parameters α∈(0,1/2)\alpha \in (0, 1/2) and β∈(0,1)\beta \in (0,1), and let (xk)(x_k) satisfy xk+1=xk−tk∇f(xk)x_{k+1} = x_k - t_k \nabla f(x_k) where each tkt_k is a backtracking step at xkx_k along −∇f(xk)-\nabla f(x_k). Then for every kk

f(xk)−p⋆  ≤  c k(f(x0)−p⋆),c  =  1−min⁡{2mα,  2βαmM}.f(x_k) - p^{\star} \;\le\; c^{\,k}\bigl(f(x_0) - p^{\star}\bigr), \qquad c \;=\; 1 - \min\Bigl\{2m\alpha,\; \frac{2\beta\alpha m}{M}\Bigr\}.

The rate is again geometric, with the constant degraded from the exact-line-search value 1−m/M1 - m/M by the two line-search parameters only; in particular the practical algorithm, which performs no one-dimensional optimization, keeps the same asymptotic behaviour. The two terms in the minimum correspond to the two possible outcomes of the search — the unit step being accepted, or a genuine backtrack.

Formalization Note The step sizes are governed by the mission's backtracking predicate, so the statement covers every admissible run rather than one implementation. Constants are exactly those printed in the book, with no rounding or simplification. Source: B&V §9.3.1, pp. 468–469.

Preamble
import Mathlib
import Definitions.Def_ConvexOptimization_IsBacktrackingStep

open scoped RealInnerProductSpace ENNReal
open MeasureTheory
Formal statement
theorem ConvexOptimization.gradient_descent_backtracking_linear_rate {n : ℕ} (m M α β : ℝ)
    (hm : 0 < m) (hmM : m ≤ M) (hα0 : 0 < α) (hα : α < 1 / 2)
    (hβ0 : 0 < β) (hβ1 : β < 1)
    (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 : ℝ,
      IsBacktrackingStep f g α β (x k) (-g (x k)) t ∧
      x (k + 1) = x k - t • g (x k)) :
    ∀ k, f (x k) - f xstar ≤
      (1 - min (2 * m * α) (2 * β * α * 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. 468-469, §9.3.1 (gradient descent with backtracking line search: linear convergence with c = 1 - min{2 m alpha, 2 beta alpha 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,M,α,βm, M, \alpha, \beta with 0<m0 < m, m≤Mm \le M, 0<α<120 < \alpha < \tfrac12 (strict on both sides), and 0<β<10 < \beta < 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); strong convexity 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; smoothness 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 global minimizer x\*x^\* of 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 there exists a real tt with xk+1=xk−t g(xk)x_{k+1} = x_k - t\, g(x_k) and tt a backtracking step at xkx_k in the direction Δ=−g(xk)\Delta = -g(x_k), i.e.: t=βjt = \beta^j for some natural jj; the Armijo inequality f(xk−t g(xk))≤f(xk)+α t ⟨g(xk),−g(xk)⟩=f(xk)−α t ∥g(xk)∥2f\big(x_k - t\,g(x_k)\big) \le f(x_k) + \alpha\, t\, \langle g(x_k), -g(x_k) \rangle = f(x_k) - \alpha\, t\, \lVert g(x_k) \rVert^2 holds; and either t=1t = 1 or the Armijo inequality fails at step t/βt/\beta; then the conclusion is: for every k∈Nk \in \mathbb{N},

f(xk)−f(x\*)≤(1−min⁡(2 m α,  2 β α mM))k (f(x0)−f(x\*)),f(x_k) - f(x^\*) \le \Big(1 - \min\Big(2\,m\,\alpha,\; \frac{2\,\beta\,\alpha\,m}{M}\Big)\Big)^{k}\, \big(f(x_0) - f(x^\*)\big),

with the contraction factor exactly 1−min⁡(2mα, 2βαm/M)1 - \min\big(2m\alpha,\ 2\beta\alpha m / M\big). Nothing in the statement asserts this factor lies in [0,1)[0,1); that is a consequence (or not) of the parameter hypotheses, not a stated hypothesis.

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