Theorem 3.2 (second part) — convergence of order $1+p$

Proved

NonsmoothNewton.Local.newton_local_order

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, let $x^*$ satisfy $F(x^*) = 0$ , let $F$ be semismooth at $x^*$ , and let every $V \in \partial F(x^*)$ be nonsingular. Suppose in addition that $0 < p \le 1$ and $F$ is $p$ -order semismooth at $x^*$ . Then there are $\delta > 0$ and a constant $C$ such that every run $(x^k, V_k)$ of the nonsmooth Newton method

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

started at a point with $\|x^0 - x^*\| < \delta$ (for every choice of the $V_k$ ) satisfies

\|x^{k+1} - x^*\| \le C\,\|x^k - x^*\|^{1+p} \qquad \text{for all } k \ge 0 .

For $p = 1$ this is local quadratic convergence of the generalized-Jacobian Newton method.

Formalization Note The paper's "the convergence of (3.2) is of order $1+p$ " is pinned as the displayed inequality, with $\delta$ and $C$ chosen before the run (uniform over all starting points and all choices of $V_k$ ), which is what the proof gives. A run is a sequence with $V_k \in \partial F(x^k)$ and $V_k(x^{k+1}-x^k) = -F(x^k)$ .

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 (second sentence), p. 359. Under the hypotheses of Theorem 3.2,
if in addition `F` is `p`-order semismooth at `x*` (`0 < p ≤ 1`), the convergence of (3.2) is
of order `1 + p`: there are `δ > 0` and `C` such that every run started within `δ` of `x*`
satisfies `‖x^{k+1} - x*‖ ≤ C ‖x^k - x*‖^{1+p}` for all `k`. -/
theorem newton_local_order {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)
    (p : ℝ) (hp0 : 0 < p) (hp1 : p ≤ 1) (hpord : POrderSemismoothAt p F xstar) :
    ∃ δ > 0, ∃ C : ℝ, ∀ (x : ℕ → EuclideanSpace ℝ (Fin n))
      (V : ℕ → EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)),
      ‖x 0 - xstar‖ < δ → IsNewtonRun F x V →
        ∀ k, ‖x (k + 1) - xstar‖ ≤ C * ‖x k - xstar‖ ^ (1 + p) := by sorry

end NonsmoothNewton.Local

Source

Qi, Sun, A nonsmooth version of Newton's method, Math. Programming 58 (1993), p. 359, Theorem 3.2 (second sentence)

Read-back

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

Setting. $n \in \mathbb{N}$ may be $0$ . $\mathbb{R}^n$ carries the Euclidean norm. $F : \mathbb{R}^n \to \mathbb{R}^n$ is locally Lipschitz on all of $\mathbb{R}^n$ . $\mathcal{J}_F(y)$ is the set of linear maps $\mathbb{R}^n \to \mathbb{R}^n$ given by the external definition clarkeJac, which is not shown here.

Hypotheses. A point $x^* \in \mathbb{R}^n$ and a real number $p$ satisfy all of the following.

Root: $F(x^*) = 0$ .
Semismoothness at $x^*$ : $F$ is $K$ -Lipschitz on a neighbourhood of $x^*$ for some $K \ge 0$ . Also, for every $h$ there is $L_h$ such that for every $\varepsilon > 0$ there is a $\delta > 0$ with $\|V h' - L_h\| < \varepsilon$ whenever $0 < t < \delta$ , $\|h' - h\| < \delta$ and $V \in \mathcal{J}_F(x^* + t h')$ .
Invertibility: every $V \in \mathcal{J}_F(x^*)$ is invertible.
Range of $p$ : $0 < p \le 1$ .
$p$ -order semismoothness at $x^*$ : $F$ is semismooth at $x^*$ , and there are real $C_0$ and $\delta_0 > 0$ with

\|V h - d\| \le C_0 \|h\|^{1+p}

for all $\|h\| < \delta_0$ , all $V \in \mathcal{J}_F(x^* + h)$ , and every one-sided directional derivative $d = \lim_{t\downarrow 0} t^{-1}(F(x^*+th) - F(x^*))$ .

Conclusion. There exist $\delta > 0$ and a real constant $C$ with the following property. Take any sequence $(x_k)_{k \in \mathbb{N}}$ in $\mathbb{R}^n$ and any sequence $(V_k)_{k\in\mathbb{N}}$ of linear maps such that:

$\|x_0 - x^*\| < \delta$ , and
for every $k$ , $V_k \in \mathcal{J}_F(x_k)$ and $V_k(x_{k+1} - x_k) = -F(x_k)$ .

For every such pair and every $k \in \mathbb{N}$ ,

\|x_{k+1} - x^*\| \le C\, \|x_k - x^*\|^{1+p} .

The theorem does not assert that any such sequence exists. It also does not state separately that the iterates remain within $\delta$ of $x^*$ or converge; only the displayed inequality for all $k$ is asserted.

Degenerate cases.

Landing on $x^*$ . If some $x_k = x^*$ , the inequality forces $x_{k+1} = x^*$ .
No runs. If no sequences satisfying the run conditions start within $\delta$ of $x^*$ , the conclusion is vacuous. This includes the case where $\mathcal{J}_F$ is empty at the relevant points.
Empty $\mathcal{J}_F(x^*)$ . The invertibility hypothesis is vacuous.
$n = 0$ . Every point equals $x^*$ , and the statement holds trivially.

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

Theorem 3.2 (second part) — convergence of order 1+p1+p1+p

Theorem 3.2 (second part) — convergence of order $1+p$