Suboptimality from the Newton decrement

Proved

ConvexOptimization.sc_suboptimality_from_decrement

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

convex-optimizationinterior-pointself-concordance

The Newton decrement bounds suboptimality, with an absolute constant.

Let $\Omega \subseteq \mathbb{R}^n$ be open and convex, let $f$ be self-concordant on $\Omega$ with positive definite Hessian throughout, and suppose $f$ attains its minimum on $\Omega$ at $x^{\star} \in \Omega$ . For $x \in \Omega$ let $\Delta$ be the Newton direction, i.e. the solution of $\nabla^2 f(x)\Delta = -\nabla f(x)$ , and let $\lambda \ge 0$ be the Newton decrement at $x$ , defined by

\lambda^{2} \;=\; \langle \nabla f(x),\, -\Delta\rangle \;=\; \nabla f(x)^{T}\nabla^2 f(x)^{-1}\nabla f(x).

If $\lambda \le 0.68$ , then

f(x) - f(x^{\star}) \;\le\; \lambda^{2}.

The decrement is available for free once the Newton step has been computed, so this inequality is the method's stopping criterion. What distinguishes it from the strongly convex theory is that the constant is absolute: no $m$ , $M$ or $L$ appears, and the bound is invariant under affine changes of coordinates, exactly as self-concordance is. The threshold $0.68$ is the book's; the estimate degrades and then fails for larger decrements, where the damped phase is still in force.

Formalization Note The Newton direction is characterized by the linear equation rather than by inverting the Hessian, and the decrement is introduced as a nonnegative real lam with lam ^ 2 = ⟪g x, -Δ⟫, which avoids a square root. Positive definiteness of the Hessian appears as ∀ v ≠ 0, 0 < ⟪H x v, v⟫, and membership x⋆ ∈ Ω is explicit — the minimum must be attained inside the domain. Source: B&V §9.6.3, p. 502.

Preamble

import Mathlib
import Definitions.Def_ConvexOptimization_selfConcordance

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.sc_suboptimality_from_decrement {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⟫)
    (xstar : EuclideanSpace ℝ (Fin n)) (hxstar : xstar ∈ Ω)
    (hstar : IsMinOn f Ω xstar)
    (x : EuclideanSpace ℝ (Fin n)) (hx : x ∈ Ω)
    (Δ : EuclideanSpace ℝ (Fin n)) (hΔ : H x Δ = -g x)
    (lam : ℝ) (hlam0 : 0 ≤ lam) (hlam : lam ^ 2 = ⟪g x, -Δ⟫)
    (hsmall : lam ≤ 0.68) :
    f x - f xstar ≤ 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. 501-502, §9.6.3 eq. (9.50) (the Newton decrement bounds suboptimality: f(x) - p* <= lambda(x)^2 when lambda(x) <= 0.68)

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 (hypothesis) and convex (separate hypothesis, partially redundant with the next one), 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$ and every $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: a map $g : \mathbb{R}^n \to \mathbb{R}^n$ such that for every $x \in \Omega$ , $f$ is differentiable at $x$ with gradient $g(x)$ (its derivative at $x$ is the functional $v \mapsto \langle g(x), v\rangle$ ); a map $H$ assigning to each point a continuous linear operator on $\mathbb{R}^n$ , such that for every $x \in \Omega$ the map $g$ is Fréchet-differentiable at $x$ with derivative $H(x)$ (so $H(x)$ is a Hessian only in the sense of being the derivative of the given field $g$ ; symmetry of $H(x)$ is not assumed); positive-definiteness: for every $x \in \Omega$ and every $v \ne 0$ , $\langle H(x)v, v\rangle > 0$ ; a point $x^* \in \Omega$ such that for every $y \in \Omega$ , $f(x^*) \le f(y)$ (the minimality predicate itself does not include membership of $x^*$ ; that is the separate hypothesis); a point $x \in \Omega$ ; a vector $\Delta$ with $H(x)\,\Delta = -g(x)$ (any solution of the Newton system); and a real $\lambda$ with $\lambda \ge 0$ , $\lambda^2 = \langle g(x), -\Delta\rangle$ , and $\lambda \le 0.68$ (the exact decimal $0.68 = 17/25$ ). Conclusion:

f(x) - f(x^*) \le \lambda^2.

Notes: the two conditions on $\lambda$ pin it as $\lambda = \sqrt{\langle g(x), -\Delta\rangle}$ and force $\langle g(x), -\Delta\rangle \ge 0$ ; if that inner product were negative, no such $\lambda$ exists and the statement is vacuous for that $x, \Delta$ . No closedness or bounded-sublevel-set hypothesis appears in this theorem. For $n = 0$ the space is a single point and the conclusion is trivially about that point.

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