Theorem 3.2 — local superlinear convergence of the nonsmooth Newton method at a semismooth regular root

Proved

NonsmoothNewton.Local.newton_local_superlinear

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

convergence-ratenewton-methodnonsmooth-analysisp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $F : \mathbb R^n \to \mathbb R^n$ be locally Lipschitz and let $x^*$ be a solution of $F(x) = 0$ (3.1). Suppose $F$ is semismooth at $x^*$ and every $V \in \partial F(x^*)$ is nonsingular. Consider the nonsmooth Newton method

x^{k+1} = x^k - V_k^{-1} F(x^k), \qquad V_k \in \partial F(x^k). \tag{3.2}

Then there is $\delta > 0$ such that:

every $V \in \partial F(y)$ with $\|y - x^*\| < \delta$ is nonsingular, and a Newton step from such a point $y$ (with any $V \in \partial F(y)$ ) lands at a point again within distance $\delta$ of $x^*$ ; so the iteration is well defined from every starting point in this neighbourhood;
every run $(x^k, V_k)$ of (3.2) with $\|x^0 - x^*\| < \delta$ , for every choice of $V_k \in \partial F(x^k)$ , has all $V_k$ nonsingular, converges to $x^*$ , and converges superlinearly:

\|x^{k+1} - x^*\| = o(\|x^k - x^*\|) \qquad (k \to \infty).

This is the basic local convergence theorem for Newton's method with generalized Jacobians: it replaces the classical smoothness assumption by semismoothness and the nonsingular Jacobian by a nonsingular generalized Jacobian.

Formalization Note The printed theorem says the iteration "is well-defined and convergent to $x^*$ in a neighborhood of $x^*$ "; the superlinear rate is the proof's display (3.3) and is stated here, as a little- $o$ along the sequence (Asymptotics.IsLittleO at infinity, no division by $\|x^k - x^*\|$ ). "Well defined" is stated as part 1 (nonsingularity in the neighbourhood and invariance of the neighbourhood under one step) and as nonsingularity of every $V_k$ of every run. A run is a sequence with $V_k \in \partial F(x^k)$ and $V_k(x^{k+1}-x^k) = -F(x^k)$ ; $\delta$ is chosen before the run. $\mathbb R^n$ is EuclideanSpace ℝ (Fin n).

Preamble

import Mathlib
import Definitions.Def_NonsmoothNewton_Shared_clarkeJac
import Definitions.Def_NonsmoothNewton_Local_SemismoothAt
import Definitions.Def_NonsmoothNewton_Local_IsNewtonRun
open Filter Topology

Formal statement

namespace NonsmoothNewton.Local

/-- Qi–Sun (1993), Theorem 3.2 (local convergence), p. 359, with the superlinear rate (3.3) of its
proof. Let `F : ℝⁿ → ℝⁿ` be locally Lipschitz, `F(x*) = 0`, `F` semismooth at `x*`, and every
`V ∈ ∂F(x*)` nonsingular. Then there is `δ > 0` such that
* every `V ∈ ∂F(y)` with `‖y - x*‖ < δ` is nonsingular, and a Newton step (3.2) from such a `y`
  lands again within `δ` of `x*` (the iteration is well defined in this neighbourhood);
* every run of (3.2) with `‖x⁰ - x*‖ < δ`, for every choice of `V_k ∈ ∂F(x^k)`, has all `V_k`
  nonsingular, converges to `x*`, and `‖x^{k+1} - x*‖ = o(‖x^k - x*‖)`. -/
theorem newton_local_superlinear {n : ℕ}
    (F : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) (hF : LocallyLipschitz F)
    (xstar : EuclideanSpace ℝ (Fin n)) (hroot : F xstar = 0) (hsemi : SemismoothAt F xstar)
    (hns : ∀ V ∈ NonsmoothNewton.Shared.clarkeJac F xstar, IsUnit V) :
    ∃ δ > 0,
      (∀ y : EuclideanSpace ℝ (Fin n), ‖y - xstar‖ < δ → ∀ W ∈ NonsmoothNewton.Shared.clarkeJac F y, IsUnit W) ∧
      (∀ y y' : EuclideanSpace ℝ (Fin n), ‖y - xstar‖ < δ → ∀ W ∈ NonsmoothNewton.Shared.clarkeJac F y,
        W (y' - y) = - F y → ‖y' - xstar‖ < δ) ∧
      (∀ (x : ℕ → EuclideanSpace ℝ (Fin n))
        (V : ℕ → EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)),
        ‖x 0 - xstar‖ < δ → IsNewtonRun F x V →
          (∀ k, IsUnit (V k)) ∧ Tendsto x atTop (𝓝 xstar) ∧
          (fun k => x (k + 1) - xstar) =o[atTop] (fun k => x k - xstar)) := by sorry

end NonsmoothNewton.Local

Source

Qi, Sun, A nonsmooth version of Newton's method, Math. Programming 58 (1993), p. 359, Theorem 3.2 (first sentence) and proof, Eq. (3.3)

Read-back

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

Let $n \in \mathbb{N}$ and write $\mathbb{R}^n$ for $n$ -dimensional Euclidean space with the Euclidean norm $\|\cdot\|$ . The statement is about three objects that are defined in imported files. Those files are not shown here, so this read-back can refer to them only by name and cannot unfold them:

$\partial F(y)$ is clarkeJac F y. It is some set of continuous linear maps $\mathbb{R}^n \to \mathbb{R}^n$ attached to $F$ and the point $y$ . Its name suggests the Clarke generalized Jacobian.
" $F$ is semismooth at $x^*$ " is SemismoothAt F xstar. It is a property of $F$ at the point $x^*$ .
" $(x, V)$ is a Newton run of $F$ " is IsNewtonRun F x V. It is a relation between $F$ , a sequence of points $x = (x^k)_{k \in \mathbb{N}}$ in $\mathbb{R}^n$ , and a sequence of continuous linear maps $V = (V_k)_{k \in \mathbb{N}}$ on $\mathbb{R}^n$ .

Throughout, " $W$ is invertible" means that $W$ is a unit in the ring of continuous linear maps $\mathbb{R}^n \to \mathbb{R}^n$ . In other words, $W$ has a two-sided continuous linear inverse, which in finite dimension is the same as a nonsingular $n \times n$ matrix.

Hypotheses. Take any map $F : \mathbb{R}^n \to \mathbb{R}^n$ and any point $x^* \in \mathbb{R}^n$ such that:

$F$ is locally Lipschitz: every point has a neighbourhood on which $F$ is Lipschitz.
$F(x^*) = 0$ .
$F$ is semismooth at $x^*$ , in the sense of the imported definition.
Every $V \in \partial F(x^*)$ is invertible.

Conclusion. There is a real number $\delta > 0$ such that all three of the following hold. The same $\delta$ serves all three clauses and every sequence in clause (c). No upper bound on $\delta$ is asserted.

(a) Invertibility near $x^*$ . For every $y \in \mathbb{R}^n$ with $\|y - x^*\| < \delta$ , every $W \in \partial F(y)$ is invertible.

(b) One step stays in the ball. Take any $y, y' \in \mathbb{R}^n$ with $\|y - x^*\| < \delta$ , and any $W \in \partial F(y)$ , such that

W(y' - y) = -F(y).

Then $\|y' - x^*\| < \delta$ .

This clause is only an implication about any $y'$ that already solves the equation. It does not itself state that such a $y'$ exists. Existence and uniqueness would follow separately from (a), since $W$ is invertible there.

(c) Newton runs. Take any sequence of points $(x^k)_{k \in \mathbb{N}}$ in $\mathbb{R}^n$ and any sequence $(V_k)_{k \in \mathbb{N}}$ of continuous linear maps on $\mathbb{R}^n$ such that:

$\|x^0 - x^*\| < \delta$ , and
$(x, V)$ is a Newton run of $F$ .

Then:

every $V_k$ is invertible, for all $k \in \mathbb{N}$ ;
$x^k \to x^*$ as $k \to \infty$ ;
$x^{k+1} - x^* = o(x^k - x^*)$ as $k \to \infty$ . Concretely, for every $\varepsilon > 0$ there is a $K$ such that for all $k \ge K$ ,

\|x^{k+1} - x^*\| \le \varepsilon \, \|x^k - x^*\|.

Whether the $V_k$ must lie in $\partial F(x^k)$ , and whether $x^{k+1}$ must satisfy $V_k(x^{k+1} - x^k) = -F(x^k)$ , depends entirely on the imported definition of a Newton run. The statement shown does not say either of these things itself.

Degenerate cases.

$n = 0$ . $\mathbb{R}^0$ is the single point $\{0\}$ . Every map on it is both the zero map and the identity, so it is invertible, and every sequence is constant and equal to $x^*$ . So every conclusion holds for any $\delta > 0$ . Clause (c) then holds trivially: $0 \le \varepsilon \cdot 0$ .
Empty or unsatisfiable definitions. The following turn parts of the statement into vacuous statements:
- If $\partial F(x^*)$ is empty, hypothesis 4 is vacuous.
- If $\partial F(y)$ is empty for points $y$ near $x^*$ , clauses (a) and (b) are vacuous at those points.
- If no pair $(x, V)$ satisfies the Newton-run relation, clause (c) is vacuous.
- If the semismoothness predicate can never hold together with the other hypotheses, the whole theorem is vacuous.
None of these can be ruled out without the imported definitions.
The little-o condition when iterates reach $x^*$ . The condition is stated with non-strict inequality and no division, so no default values from division by zero arise. If $x^k = x^*$ for some large $k$ , it forces $x^{k+1} = x^*$ as well.
No other defaults. There are no natural-number subtractions, integrals, or suprema in the statement itself.

Human review

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

View graph