Newton complexity for self-concordant functions

Disproved

ConvexOptimization.sc_newton_iteration_bound

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

convex-optimizationinterior-pointself-concordance

⚠️ DEPRECATED — this statement is false and has been disproved.

The replacement is ConvexOptimization.sc_newton_iteration_bound_on, which states the same theorem with a domain-confined line search.

Why it is false. IsDampedNewtonSequenceOn requires every iterate to lie in $\Omega$ , while IsBacktrackingStep tests the Armijo inequality

f(x + t\Delta) \le f(x) + \alpha t \langle \nabla f(x), \Delta\rangle

at all the points $x + \beta^{j}\Delta$ , feasible or not. The hypotheses constrain $f$ only on $\Omega$ — IsSelfConcordantOn Ω f, IsMinOn f Ω xstar and the sublevel set in hclosed are all relative to $\Omega$ — so $f$ may be made arbitrarily small outside it, and the line search then accepts a full step that leaves the domain.

Counterexample. $n=1$ , $\Omega=(0,\infty)$ , $f(u)=-\log u+u$ on $\Omega$ and $f=-1000$ off it; $\alpha=\tfrac14$ , $\beta=\tfrac25$ , $x^{(0)}=3$ . All hypotheses hold ( $|f'''|=2(f'')^{3/2}$ with equality, minimum $f(1)=1$ , sublevel set $\subseteq[\tfrac1{25},3]$ closed). The Newton step is $\Delta=-6$ , so $x^{(0)}+\Delta=-3\notin\Omega$ ; the Armijo test passes at $t=1$ (where $f=-1000$ ) and at every $\beta^{j}$ with $j\ge1$ (because $-\log(1-2t)\le5t$ on $(0,\tfrac25]$ ), so $t=1$ is the only admissible backtracking step and no run exists.

How the replacement fixes it. IsBacktrackingStepOn accepts the largest $\beta^{j}$ whose trial point is both in $\Omega$ and Armijo-acceptable — exactly what B&V's convention $f=+\infty$ off $\operatorname{dom} f$ (§9.1, p. 457) delivers automatically. The hclosed hypothesis is also stated at every level $c$ , as the Dikin-ellipsoid argument behind (9.55) needs.

The Newton iteration bound for self-concordant functions, with absolute constants — inequality (9.56) of Boyd & Vandenberghe.

Let $\Omega \subseteq \mathbb{R}^n$ be open and convex, let $f$ be self-concordant on $\Omega$ with positive definite Hessian, attaining its minimum at $x^{\star} \in \Omega$ . Fix backtracking parameters $\alpha \in (0,1/2)$ , $\beta \in (0,1)$ , an accuracy $\varepsilon \in (0,1/4)$ , and a starting point $x^{(0)} \in \Omega$ whose sublevel set $\{x \in \Omega : f(x) \le f(x^{(0)})\}$ is closed. Then there is a damped Newton run with backtracking on $\Omega$ starting at $x^{(0)}$ , and an index $K$ with

K \;\le\; \frac{20 - 8\alpha}{\alpha\beta(1-2\alpha)^{2}}\,\bigl(f(x^{(0)}) - f(x^{\star})\bigr) \;+\; \log_2\log_2(1/\varepsilon) \;+\; 1, \qquad f(x^{(K)}) - f(x^{\star}) \le \varepsilon .

The shape is the familiar two phases — a damped phase of fixed decrease, then a doubly logarithmic quadratic phase — but every constant is now absolute. Nothing in the bound refers to the dimension $n$ , to strong-convexity or smoothness moduli, or to a Lipschitz constant for the Hessian, and nothing changes under an affine change of coordinates. That is the whole payoff of self-concordance, and it is what makes a per-centering bound uniform along the central path in the barrier method.

Formalization Note The statement is existential in the run and the index — "some faithful run succeeds" — matching the book's idealized analysis; the run is governed by the mission's domain-confined damped-Newton predicate. Source: B&V §9.6.4, pp. 503–505, eq. (9.56), with $1/\gamma = (20-8\alpha)/(\alpha\beta(1-2\alpha)^2)$ .

Preamble

import Mathlib
import Definitions.Def_ConvexOptimization_selfConcordance
import Definitions.Def_ConvexOptimization_IsBacktrackingStep

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.sc_newton_iteration_bound {n : ℕ} (α β ε : ℝ)
    (hα0 : 0 < α) (hα : α < 1 / 2) (hβ0 : 0 < β) (hβ1 : β < 1)
    (hε0 : 0 < ε) (hε1 : ε < 1 / 4)
    (Ω : 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)
    (x0 : EuclideanSpace ℝ (Fin n)) (hx0 : x0 ∈ Ω)
    (hclosed : IsClosed {x | x ∈ Ω ∧ f x ≤ f x0}) :
    ∃ (x : ℕ → EuclideanSpace ℝ (Fin n)) (K : ℕ),
      x 0 = x0 ∧ IsDampedNewtonSequenceOn Ω f g H α β x ∧
      (K : ℝ) ≤ (20 - 8 * α) / (α * β * (1 - 2 * α) ^ 2) * (f x0 - f xstar) +
        Real.logb 2 (Real.logb 2 (1 / ε)) + 1 ∧
      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. 503-505, §9.6.4 eq. (9.56) (Newton iteration bound for self-concordant functions, with 1/gamma = (20 - 8 alpha)/(alpha beta (1 - 2 alpha)^2) and absolute constants)

Read-back

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

Fix reals $\alpha, \beta, \varepsilon$ with $0 < \alpha < 1/2$ , $0 < \beta < 1$ , and $0 < \varepsilon < 1/4$ ; a natural $n$ ; a set $\Omega \subseteq \mathbb{R}^n$ that is open and convex; and a total function $f : \mathbb{R}^n \to \mathbb{R}$ self-concordant on $\Omega$ (meaning: $\Omega$ convex and $f(ax+by) \le af(x)+bf(y)$ for $x,y \in \Omega$ , $a,b \ge 0$ , $a+b=1$ ; $f$ three times continuously differentiable on $\Omega$ , within-set sense; and for all $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$ with $f$ differentiable at each $x \in \Omega$ with gradient $g(x)$ ; $H$ (point $\mapsto$ continuous linear operator) with $g$ Fréchet-differentiable at each $x \in \Omega$ with derivative $H(x)$ ; $\langle H(x)v, v\rangle > 0$ for all $x \in \Omega$ , $v \ne 0$ ; a point $x^* \in \Omega$ with $f(x^*) \le f(y)$ for all $y \in \Omega$ ; a starting point $x_0 \in \Omega$ ; and closedness of the single sublevel set $\{x : x \in \Omega \text{ and } f(x) \le f(x_0)\}$ (only at level $f(x_0)$ , unlike the all-levels hypothesis of the contraction theorem). Conclusion (existential): there exist a sequence $x_0', x_1', x_2', \ldots$ in $\mathbb{R}^n$ and a natural number $K$ such that: (a) $x_0' = x_0$ ; (b) the sequence is a damped Newton sequence on $\Omega$ for $f, g, H, \alpha, \beta$ , i.e. for every $k$ : $x_k' \in \Omega$ and 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 $f(x_k' + (t/\beta)\Delta) \le f(x_k') + \alpha(t/\beta)\langle g(x_k'), \Delta\rangle$ fails), and $x_{k+1}' = x_k' + t\Delta$ ; (c) as a real number,

K \le \frac{20 - 8\alpha}{\alpha\beta(1-2\alpha)^2}\,\bigl(f(x_0) - f(x^*)\bigr) + \log_2\bigl(\log_2(1/\varepsilon)\bigr) + 1,

where $\log_2 y$ denotes $\log y / \log 2$ as a total function (junk $\log|y|/\log 2$ for $y < 0$ , and $0$ at $y = 0$ ; here $\varepsilon < 1/4$ gives $1/\varepsilon > 4$ , so $\log_2(1/\varepsilon) > 2$ and both logarithms are genuine and positive); and (d) $f(x_K') - f(x^*) \le \varepsilon$ . Note the exact constant: numerator $20 - 8\alpha$ , denominator $\alpha\beta(1-2\alpha)^2$ (positive since $0 < \alpha < 1/2$ , $\beta > 0$ ). The statement is existential: it asserts that SOME damped-Newton run (some choice of solutions $\Delta$ and backtracking steps at every index, for all $k$ , not just $k \le K$ ) reaches accuracy $\varepsilon$ at index $K$ within the stated bound; it does not assert this for every such run.

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