Prove2Me

Newton damped-phase decrease

Proved
ConvexOptimization.newton_damped_phase_decrease

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

convexoptimizationnewtonmethodoptimizationalgorithms

The damped Newton phase: a fixed decrease per iteration — inequality (9.32) of Boyd & Vandenberghe.

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

mI⪯∇2f(x)⪯MIfor all x,∥∇2f(x)−∇2f(y)∥≤L∥x−y∥2for all x,y,m I \preceq \nabla^2 f(x) \preceq M I \quad \text{for all } x, \qquad \lVert \nabla^2 f(x) - \nabla^2 f(y)\rVert \le L \lVert x - y\rVert_2 \quad \text{for all } x, y,

the second being the Lipschitz-Hessian condition (9.31). Fix backtracking parameters α∈(0,1/2)\alpha \in (0, 1/2), β∈(0,1)\beta \in (0,1) and set

η  =  min⁡{1, 3(1−2α)} m2L,γ  =  αβη2mM2.\eta \;=\; \min\{1,\, 3(1 - 2\alpha)\}\,\frac{m^{2}}{L}, \qquad \gamma \;=\; \frac{\alpha\beta\eta^{2}m}{M^{2}}.

Let xx be a point with ∥∇f(x)∥2≥η\lVert \nabla f(x)\rVert_2 \ge \eta, let Δ\Delta be its Newton step, i.e. the solution of ∇2f(x) Δ=−∇f(x)\nabla^2 f(x)\,\Delta = -\nabla f(x), and let tt be any backtracking step at xx along Δ\Delta. Then

f(x+tΔ)  ≤  f(x)−γ.f(x + t\Delta) \;\le\; f(x) - \gamma .

While the gradient stays above the threshold η\eta, every iteration buys a decrease of at least the constant γ\gamma — independent of the iterate. Since ff is bounded below by p⋆p^{\star}, this immediately caps the number of such iterations by (f(x(0))−p⋆)/γ(f(x^{(0)}) - p^{\star})/\gamma, which is the first of the two terms in the mission's goal theorem.

Formalization Note The Hessian bounds are stated in quadratic-form guise, m * ‖v‖ ^ 2 ≤ ⟪H x v, v⟫ and ⟪H x v, v⟫ ≤ M * ‖v‖ ^ 2, and the Lipschitz condition uses the operator norm on continuous linear maps. The Newton direction appears as a solution of the linear system, so no invertibility hypothesis is needed. Source: B&V §9.5.3, pp. 489–490, eq. (9.32).

Preamble
import Mathlib
import Definitions.Def_ConvexOptimization_IsBacktrackingStep

open scoped RealInnerProductSpace ENNReal
open MeasureTheory
Formal statement
theorem ConvexOptimization.newton_damped_phase_decrease {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η : η = min 1 (3 * (1 - 2 * α)) * m ^ 2 / L)
    (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‖)
    (x Δ : EuclideanSpace ℝ (Fin n)) (t : ℝ)
    (hΔ : H x Δ = -g x) (hgx : η ≤ ‖g x‖)
    (ht : IsBacktrackingStep f g α β x Δ t) :
    f (x + t • Δ) ≤ f x - α * β * η ^ 2 * m / M ^ 2 := by
  sorry
Source
Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 489-490, §9.5.3 eq. (9.32) (damped Newton phase: each step decreases f by at least gamma = alpha beta eta^2 m / M^2, with eta = min{1, 3(1 - 2 alpha)} m^2 / L)
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,L,α,β,ηm, M, L, \alpha, \beta, \eta with 0<m0 < m, m≤Mm \le M, 0<L0 < L, 0<α<120 < \alpha < \tfrac12, 0<β<10 < \beta < 1, and η\eta defined by the hypothesis η=min⁡(1, 3(1−2α))⋅m2/L\eta = \min\big(1,\ 3(1 - 2\alpha)\big) \cdot m^2 / L (since α<12\alpha < \tfrac12, the factor 3(1−2α)3(1-2\alpha) is positive, so η>0\eta > 0), 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); a Hessian field HH (for every xx, gg is Fréchet-differentiable at xx with derivative the continuous linear map HxH_x); the eigenvalue-type bounds m∥v∥2≤⟨Hx(v),v⟩m \lVert v \rVert^2 \le \langle H_x(v), v \rangle and ⟨Hx(v),v⟩≤M∥v∥2\langle H_x(v), v \rangle \le M \lVert v \rVert^2 for all x,vx, v; the Lipschitz condition ∥Hx−Hy∥≤L ∥x−y∥\lVert H_x - H_y \rVert \le L\, \lVert x - y \rVert for all x,yx, y, where ∥Hx−Hy∥\lVert H_x - H_y \rVert is the operator norm of the difference of the linear maps; a point xx, a vector Δ\Delta, and a real tt such that: Hx(Δ)=−g(x)H_x(\Delta) = -g(x) (Δ\Delta is some solution of the Newton system, not assumed unique), η≤∥g(x)∥\eta \le \lVert g(x) \rVert (large-gradient/damped phase, non-strict), and tt is a backtracking step for f,g,α,βf, g, \alpha, \beta at xx in direction Δ\Delta (i.e. t=βjt = \beta^j for some natural jj; f(x+tΔ)≤f(x)+αt⟨g(x),Δ⟩f(x + t\Delta) \le f(x) + \alpha t \langle g(x), \Delta\rangle; and t=1t = 1 or the Armijo inequality fails at t/βt/\beta); then:

f(x+t Δ)≤f(x)−α β η2 mM2,f(x + t\,\Delta) \le f(x) - \frac{\alpha\, \beta\, \eta^2\, m}{M^2},

i.e. one accepted backtracking Newton step decreases ff by at least the exact constant αβη2m/M2\alpha\beta\eta^2 m / M^2.

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