Theorem 3 (item 1) — $\delta_k$ well defined and (3.6)

Proved

CubicNewton.LocalQuad.theorem3_delta_quadratic

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

cubic-regularizationlocal-convergencenewton-methodp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $f:\mathbb{R}^n\to\mathbb{R}$ ( $n \ge 1$ ) be twice differentiable with $L$ -Lipschitz Hessian ( $L > 0$ ). Let $\{x_k\}_{k\ge0}$ be generated by the relaxed method (3.5): $x_{k+1} = T_{M_k}(x_k)$ with $M_k \in (0, 2L]$ , where $T_{M_k}(x_k)$ is a global minimizer of the cubic model at $x_k$ . Write

\delta_k = \frac{L\|f'(x_k)\|}{\lambda_n^2(f''(x_k))}.

Suppose $f''(x_0) \succ 0$ and $\delta_0 \le 1/4$ . Then for all $k \ge 0$ the value $\delta_k$ is well defined, i.e. $f''(x_k) \succ 0$ , and

\delta_{k+1} \le \frac32\left(\frac{\delta_k}{1-\delta_k}\right)^2 \le \frac83\,\delta_k^2 \le \frac23\,\delta_k .

So $\delta_k$ converges to zero quadratically, and every iterate stays in the region where the Hessian is positive definite.

Formalization Note "Well defined" is rendered as $\lambda_n(f''(x_k)) > 0$ for every $k$ , and each of the three inequalities of the chain is stated for every $k \ge 0$ . The mission takes $F = \mathbb{R}^n$ : $f$ is twice differentiable and Assumption 1 holds on all of $\mathbb{R}^n$ (the relaxed method has no descent test that would keep the iterates in a smaller set). $\lambda_n$ is lamMin, $\delta$ is deltaMeasure, and the index is 0-based.

Preamble

import Mathlib
import Definitions.Def_CubicNewton_LocalQuad_IsRelaxedRun
import Definitions.Def_CubicNewton_LocalQuad_deltaMeasure

Formal statement

namespace CubicNewton.LocalQuad

/-- Nesterov–Polyak 2006, Theorem 3, item 1, (3.6), p. 187, in the case `F = ℝⁿ`:
let `f″(x₀) ≻ 0` and `δ₀ ≤ 1/4`, and let `{x_k}` be generated by the relaxed method (3.5).
Then for all `k ≥ 0` the value `δ_k` is well defined (`λₙ(f″(x_k)) > 0`) and
`δ_{k+1} ≤ (3/2)(δ_k/(1 − δ_k))² ≤ (8/3)δ_k² ≤ (2/3)δ_k`. -/
theorem theorem3_delta_quadratic {n : ℕ}
    (f : EuclideanSpace ℝ (Fin n) → ℝ)
    (g : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
    (H : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n))
    (L : ℝ)
    (hf : ∀ x, HasGradientAt f (g x) x) (hg : ∀ x, HasFDerivAt g (H x) x)
    (hL : 0 < L) (hLip : ∀ x y, ‖H x - H y‖ ≤ L * ‖x - y‖)
    (hn : 0 < n) (x : ℕ → EuclideanSpace ℝ (Fin n)) (M : ℕ → ℝ)
    (hrun : IsRelaxedRun L g H x M)
    (hpos : 0 < CubicNewton.Shared.lamMin (H (x 0))) (hδ0 : deltaMeasure L g H (x 0) ≤ 1 / 4) :
    ∀ k, 0 < CubicNewton.Shared.lamMin (H (x k)) ∧
      deltaMeasure L g H (x (k + 1)) ≤
        3 / 2 * (deltaMeasure L g H (x k) / (1 - deltaMeasure L g H (x k))) ^ 2 ∧
      3 / 2 * (deltaMeasure L g H (x k) / (1 - deltaMeasure L g H (x k))) ^ 2 ≤
        8 / 3 * deltaMeasure L g H (x k) ^ 2 ∧
      8 / 3 * deltaMeasure L g H (x k) ^ 2 ≤ 2 / 3 * deltaMeasure L g H (x k) := by sorry

end CubicNewton.LocalQuad

Source

Nesterov & Polyak, Cubic regularization of Newton method and its global performance, Math. Program. Ser. A 108 (2006) 177–205, DOI 10.1007/s10107-006-0706-8, p. 187, Theorem 3, item 1, inequality (3.6)

Read-back

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

Fix $n \in \mathbb{N}$ with $n > 0$ , and work in $\mathbb{R}^n$ with the Euclidean norm. Let $f : \mathbb{R}^n \to \mathbb{R}$ , $g : \mathbb{R}^n \to \mathbb{R}^n$ , $H$ an operator-valued map, and $L \in \mathbb{R}$ . Assume:

$f$ has gradient $g(x)$ at every $x$ ;
$g$ has Fréchet derivative $H(x)$ at every $x$ ;
$L > 0$ ;
$\|H(x) - H(y)\| \le L\|x - y\|$ for all $x, y$ , in operator norm.

Let $(x_k)_{k\ge0}$ be a sequence in $\mathbb{R}^n$ and $(M_k)_{k\ge0}$ a sequence of reals, and assume that for every $k$ :

$0 < M_k \le 2L$ ;
$\mathrm{CubicStep}_{g,H}(M_k, x_k, x_{k+1})$ holds. This is an imported predicate whose body is not shown here.

Write

\delta_k = \frac{L\,\|g(x_k)\|}{\lambda_{\min}(H(x_k))^2},

with the value $0$ whenever the denominator is $0$ . Here $\lambda_{\min}$ is an imported real-valued function on operators. Its body is not shown here. Finally assume $\lambda_{\min}(H(x_0)) > 0$ and $\delta_0 \le \tfrac14$ .

The conclusion is that for every $k \ge 0$ all four of the following hold:

\lambda_{\min}(H(x_k)) > 0,

\delta_{k+1} \;\le\; \tfrac32\Big(\frac{\delta_k}{1 - \delta_k}\Big)^2 \;\le\; \tfrac83\,\delta_k^2 \;\le\; \tfrac23\,\delta_k .

The first conjunct makes every $\delta_k$ a genuine quotient. Since $L > 0$ , every $\delta_k$ is also $\ge 0$ .

Degenerate cases and consequences:

The case $n = 0$ is excluded by hypothesis.
If $\delta_k = 1$ , the quotient $\delta_k/(1-\delta_k)$ would default to $0$ . However, the last inequality $\tfrac83\delta_k^2 \le \tfrac23\delta_k$ holds exactly when $0 \le \delta_k \le \tfrac14$ , so the conclusion itself asserts $\delta_k \in [0, \tfrac14]$ for all $k$ , and that default never comes into play.
The theorem is vacuous if no pair of sequences satisfies the run conditions. Whether that happens depends on the imported predicate $\mathrm{CubicStep}$ , which is not shown here.

Human review

Endorsed by Shuze Chen · Sep 28, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 28, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Theorem 3 (item 1) — δk\delta_kδk​ well defined and (3.6)

Theorem 3 (item 1) — $\delta_k$ well defined and (3.6)