Prove2Me

Gradient descent with backtracking: linear rate

Proved
ConvexOptimization.gradient_descent_backtracking_linear_rate

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

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})

View graph