Two-phase Newton complexity bound

Proved

ConvexOptimization.newton_two_phase_iteration_bound

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

convexoptimizationnewtonmethodoptimizationalgorithms

The two-phase complexity bound for Newton's method with backtracking — inequality (9.36) of Boyd & Vandenberghe, the goal of this mission.

Let $f : \mathbb{R}^n \to \mathbb{R}$ be twice differentiable with gradient field $\nabla f$ and Hessian field $\nabla^2 f$ , and assume, for constants $0 < m \le M$ and $L > 0$ ,

m I \preceq \nabla^2 f(x) \preceq M I \quad (x \in \mathbb{R}^n), \qquad \lVert \nabla^2 f(x) - \nabla^2 f(y)\rVert \le L \lVert x - y\rVert_2 \quad (x, y \in \mathbb{R}^n).

Let $x^{\star}$ be a global minimizer, $p^{\star} = f(x^{\star})$ , fix backtracking parameters $\alpha \in (0,1/2)$ , $\beta \in (0,1)$ , and let $(x_k)$ be any damped Newton sequence with backtracking. Put

\eta = \min\{1,\,3(1-2\alpha)\}\frac{m^{2}}{L}, \qquad \gamma = \frac{\alpha\beta\eta^{2}m}{M^{2}}, \qquad \varepsilon_0 = \frac{2m^{3}}{L^{2}} .

Then for every accuracy $\varepsilon$ with $0 < \varepsilon \le \varepsilon_0/4$ and every $K \in \mathbb{N}$ satisfying

K \;\ge\; \frac{f(x_0) - p^{\star}}{\gamma} \;+\; \log_2\log_2\bigl(\varepsilon_0/\varepsilon\bigr),

the iterate $x_K$ is $\varepsilon$ -optimal:

f(x_K) - p^{\star} \;\le\; \varepsilon .

The two summands are the two phases: at most $(f(x_0) - p^{\star})/\gamma$ damped iterations, each buying a fixed decrease $\gamma$ , followed by a quadratically convergent phase whose length grows like $\log_2\log_2(1/\varepsilon)$ — six iterations already give $\varepsilon \approx 5\cdot 10^{-20}\varepsilon_0$ . The bound is dimension-free, and its dependence on the accuracy is doubly logarithmic rather than logarithmic, which is the precise sense in which Newton's method outperforms every first-order method.

Formalization Note The hypothesis $\varepsilon \le \varepsilon_0/4$ is stated as ε ≤ m ^ 3 / (2 * L ^ 2); it is needed because the book's count is valid once the quadratic phase has genuinely begun, and for $\varepsilon \in (\varepsilon_0/4, \varepsilon_0)$ the literal bound (9.36) fails. The quantities $\eta$ and $\gamma$ are inlined into the hypothesis on $K$ rather than introduced as abbreviations, and $\log_2$ is Mathlib's Real.logb 2. The iterates are governed by the mission's damped-Newton predicate, so the conclusion holds for every faithful run. Source: B&V §9.5.3, p. 491, eq. (9.36).

Preamble

import Mathlib
import Definitions.Def_ConvexOptimization_IsBacktrackingStep
import Definitions.Def_ConvexOptimization_IsDampedNewtonSequence

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.newton_two_phase_iteration_bound {n : ℕ} (m M L α β ε : ℝ)
    (hm : 0 < m) (hmM : m ≤ M) (hL : 0 < L)
    (hα0 : 0 < α) (hα : α < 1 / 2) (hβ0 : 0 < β) (hβ1 : β < 1)
    (hε0 : 0 < ε) (hεsmall : ε ≤ m ^ 3 / (2 * L ^ 2))
    (f : EuclideanSpace ℝ (Fin n) → ℝ)
    (g : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
    (hg : ∀ x, HasGradientAt f (g x) x)
    (H : EuclideanSpace ℝ (Fin n) →
      EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n))
    (hH : ∀ x, HasFDerivAt g (H x) x)
    (hHm : ∀ x v, m * ‖v‖ ^ 2 ≤ ⟪H x v, v⟫)
    (hHM : ∀ x v, ⟪H x v, v⟫ ≤ M * ‖v‖ ^ 2)
    (hHL : ∀ x y, ‖H x - H y‖ ≤ L * ‖x - y‖)
    (xstar : EuclideanSpace ℝ (Fin n)) (hstar : IsMinOn f Set.univ xstar)
    (x : ℕ → EuclideanSpace ℝ (Fin n))
    (hnewton : IsDampedNewtonSequence f g H α β x)
    (K : ℕ)
    (hK : (f (x 0) - f xstar) /
        (α * β * (min 1 (3 * (1 - 2 * α)) * m ^ 2 / L) ^ 2 * m / M ^ 2) +
        Real.logb 2 (Real.logb 2 (2 * m ^ 3 / L ^ 2 / ε)) ≤ (K : ℝ)) :
    f (x K) - 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. 491, §9.5.3 eq. (9.36) (total complexity of Newton's method with backtracking: (f(x0) - p*)/gamma + log2 log2(eps0/eps)). Formalized with the extra hypothesis eps <= eps0/4 = m^3/(2 L^2), without which the printed double-log budget fails for eps in (eps0/4, eps0)

Read-back

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

For every $n \in \mathbb{N}$ (including $0$ ) and reals $m, M, L, \alpha, \beta, \varepsilon$ with $0 < m$ , $m \le M$ , $0 < L$ , $0 < \alpha < \tfrac12$ , $0 < \beta < 1$ , $0 < \varepsilon$ , and $\varepsilon \le m^3/(2L^2)$ , given: $f$ with gradient field $g$ (for every $x$ , $g(x)$ is the gradient of $f$ at $x$ ); a Hessian field $H$ (for every $x$ , $g$ is Fréchet-differentiable at $x$ with derivative $H_x$ ); the bounds $m\lVert v \rVert^2 \le \langle H_x(v), v \rangle \le M \lVert v \rVert^2$ for all $x, v$ ; the operator-norm Lipschitz condition $\lVert H_x - H_y \rVert \le L \lVert x - y \rVert$ for all $x, y$ ; a global minimizer $x^\*$ of $f$ over the whole space ( $f(x^\*) \le f(y)$ for all $y$ , assumed to exist as data); a sequence $x : \mathbb{N} \to \mathbb{R}^n$ that is a damped-Newton backtracking sequence, meaning for every $k$ there exist $\Delta$ and $t$ with $H_{x_k}(\Delta) = -g(x_k)$ , $t = \beta^j$ for some natural $j$ , $f(x_k + t\Delta) \le f(x_k) + \alpha t \langle g(x_k), \Delta \rangle$ , ( $t = 1$ or Armijo fails at $t/\beta$ ), and $x_{k+1} = x_k + t\Delta$ ( $x_0$ unconstrained); and a natural number $K$ satisfying the real inequality

\frac{f(x_0) - f(x^\*)}{\alpha\, \beta\, \big(\min(1,\ 3(1-2\alpha)) \cdot m^2 / L\big)^{2}\, m \,/\, M^2} \;+\; \log_2\!\Big(\log_2\Big(\frac{2 m^3}{L^2\, \varepsilon}\Big)\Big) \;\le\; K,

where the first denominator is exactly $\alpha \beta \eta^2 m / M^2$ with $\eta = \min(1, 3(1-2\alpha)) \cdot m^2/L$ , the doubly-divided expression $2 m^3 / L^2 / \varepsilon$ means $2m^3/(L^2 \varepsilon)$ , and $\log_2$ is the real base-2 logarithm with the junk convention that the logarithm of a nonpositive argument is $0$ (here $\varepsilon \le m^3/(2L^2)$ makes the inner argument $\ge 4$ , hence the inner $\log_2 \ge 2$ and the outer $\log_2 \ge 1$ , so neither hits the junk case); then the conclusion is:

f(x_K) - f(x^\*) \le \varepsilon,

asserted at the single index $K$ (though since $K$ is any natural number satisfying the displayed inequality, the statement applies to every such $K$ ).

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