Newton-decrement contraction of the pure step

Proved

ConvexOptimization.sc_newton_decrement_contraction

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

convex-optimizationinterior-pointself-concordance

Quadratic contraction of the Newton decrement — inequality (9.55) of Boyd & Vandenberghe.

Let $\Omega \subseteq \mathbb{R}^n$ be open and convex, let $f$ be self-concordant on $\Omega$ with positive definite Hessian and with closed sublevel sets $\{y \in \Omega : f(y) \le c\}$ . Let $x \in \Omega$ , let $\Delta$ solve $\nabla^2 f(x)\Delta = -\nabla f(x)$ , and let $\lambda \ge 0$ be the Newton decrement at $x$ , $\lambda^2 = \langle \nabla f(x), -\Delta\rangle$ . If $\lambda < 1$ , then the full Newton step remains in the domain, $x + \Delta \in \Omega$ , and the decrement at the new point satisfies

\lambda(x + \Delta) \;\le\; \Bigl(\frac{\lambda}{1 - \lambda}\Bigr)^{2}.

Two things are asserted at once, and both matter. The domain statement is not automatic — for a barrier objective, leaving $\Omega$ means violating a constraint — and self-concordance is precisely what guarantees the unit step is safe once $\lambda < 1$ . The contraction then gives quadratic convergence beyond an absolute threshold: for $\lambda \le 1/4$ , say, the decrement is at most squared at each step, so the number of iterations to reach any accuracy is bounded without reference to problem constants.

Formalization Note The conclusion quantifies over any Newton direction $\Delta'$ and any nonnegative $\lambda'$ with $\lambda'^2 = \langle \nabla f(x+\Delta), -\Delta'\rangle$ , rather than asserting uniqueness of the decrement. The closed-sublevel-set hypothesis is the standing assumption of B&V §9.6.4. Source: B&V §9.6.4, p. 505, eq. (9.55) / exercise 9.18; proof in Nesterov, Lectures on Convex Optimization, Theorem 5.2.2.

Preamble

import Mathlib
import Definitions.Def_ConvexOptimization_selfConcordance

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.sc_newton_decrement_contraction {n : ℕ}
    (Ω : Set (EuclideanSpace ℝ (Fin n))) (hΩo : IsOpen Ω) (hΩc : Convex ℝ Ω)
    (f : EuclideanSpace ℝ (Fin n) → ℝ) (hsc : IsSelfConcordantOn Ω f)
    (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)
    (hHpd : ∀ x ∈ Ω, ∀ v, v ≠ 0 → 0 < ⟪H x v, v⟫)
    (hclosed : ∀ c : ℝ, IsClosed {y | y ∈ Ω ∧ f y ≤ c})
    (x : EuclideanSpace ℝ (Fin n)) (hx : x ∈ Ω)
    (Δ : EuclideanSpace ℝ (Fin n)) (hΔ : H x Δ = -g x)
    (lam : ℝ) (hlam0 : 0 ≤ lam) (hlam : lam ^ 2 = ⟪g x, -Δ⟫) (hlt : lam < 1) :
    x + Δ ∈ Ω ∧
    ∀ (Δ' : EuclideanSpace ℝ (Fin n)) (lam' : ℝ),
      H (x + Δ) Δ' = -g (x + Δ) → 0 ≤ lam' → lam' ^ 2 = ⟪g (x + Δ), -Δ'⟫ →
      lam' ≤ (lam / (1 - lam)) ^ 2 := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 505, 517, §9.6.4 eq. (9.55) (quadratic contraction of the Newton decrement) and exercise 9.18, p. 517 (quadratic convergence). Proof source: Nesterov 2018, Lectures on Convex Optimization (2nd edition), Springer, Theorem 5.2.2. The closed-sublevel-set hypothesis is the standing assumption of §9.6.4

Read-back

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

Fix a natural number $n$ , a set $\Omega \subseteq \mathbb{R}^n$ that is open and convex (two hypotheses), and a total function $f : \mathbb{R}^n \to \mathbb{R}$ that is self-concordant on $\Omega$ , meaning: $\Omega$ is convex and $f(ax+by) \le af(x)+bf(y)$ for $x,y \in \Omega$ , $a,b \ge 0$ , $a+b=1$ ; $f$ is three times continuously differentiable on $\Omega$ (within-set sense); and for every $x \in \Omega$ , $v \in \mathbb{R}^n$ , the line restriction $\varphi(t) = f(x+tv)$ satisfies $|\varphi'''(0)| \le 2(\varphi''(0))^{3/2}$ at $t = 0$ (total, possibly junk, derivatives; real power with $b^{3/2} = 0$ for $b \le 0$ ). Further hypotheses: $g : \mathbb{R}^n \to \mathbb{R}^n$ with $f$ differentiable at each $x \in \Omega$ with gradient $g(x)$ ; $H$ assigning to each point a continuous linear operator, with $g$ Fréchet-differentiable at each $x \in \Omega$ with derivative $H(x)$ ; for every $x \in \Omega$ and $v \ne 0$ , $\langle H(x)v, v\rangle > 0$ (symmetry not assumed); and for EVERY real $c$ , the sublevel set $\{y : y \in \Omega \text{ and } f(y) \le c\}$ is closed. (No minimizer is hypothesized in this theorem.) Given: $x \in \Omega$ ; $\Delta$ with $H(x)\,\Delta = -g(x)$ ; and a real $\lambda$ with $\lambda \ge 0$ , $\lambda^2 = \langle g(x), -\Delta\rangle$ (forcing $\langle g(x), -\Delta\rangle \ge 0$ ; vacuous otherwise), and $\lambda < 1$ (strict). Conclusion, a conjunction of two claims: (1) $x + \Delta \in \Omega$ — the full, undamped Newton step from $x$ lands in $\Omega$ ; and (2) for every vector $\Delta'$ and real $\lambda'$ such that $H(x+\Delta)\,\Delta' = -g(x+\Delta)$ , $\lambda' \ge 0$ , and $\lambda'^2 = \langle g(x+\Delta), -\Delta'\rangle$ , one has

\lambda' \le \Bigl(\frac{\lambda}{1-\lambda}\Bigr)^2.

Note carefully: the bound is on the first power of $\lambda'$ , compared against the square of the ratio $\lambda/(1-\lambda)$ — it is $\lambda' \le (\lambda/(1-\lambda))^2$ , not a statement about $\lambda'^2$ . If no pair $(\Delta', \lambda')$ satisfies the three conditions at $x + \Delta$ , claim (2) is vacuously true.

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