Proposition 3.1 — uniform bound on $\|V^{-1}\|$ near a point where $\partial F$ is nonsingular

Proved

NonsmoothNewton.Local.prop_3_1

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

newton-methodnonsmooth-analysisp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $F : \mathbb R^n \to \mathbb R^n$ be locally Lipschitz and $x \in \mathbb R^n$ . If every $V \in \partial F(x)$ is nonsingular, then there are a neighbourhood $N(x)$ of $x$ and a constant $C$ such that for every $y \in N(x)$ and every $V \in \partial F(y)$ , $V$ is nonsingular and

\|V^{-1}\| \le C .

This is the uniform invertibility that makes every Newton step near a regular root well defined and controls its size.

Formalization Note $\mathbb R^n$ is EuclideanSpace ℝ (Fin n) with the Euclidean norm, and $\|V^{-1}\|$ is the corresponding operator norm; "nonsingular with inverse of norm at most $C$ " is written as the existence of a two-sided inverse $W$ with $\|W\| \le C$ . Section 3's standing assumption " $F$ locally Lipschitzian" is a hypothesis, although the proposition's sentence does not repeat it.

Preamble

import Mathlib
import Definitions.Def_NonsmoothNewton_Shared_clarkeJac
open Filter Topology

Formal statement

namespace NonsmoothNewton.Local

/-- Qi–Sun (1993), Proposition 3.1, p. 359 (Section 3 standing assumption: `F : ℝⁿ → ℝⁿ`
locally Lipschitz). If every `V ∈ ∂F(x)` is nonsingular, there are a neighbourhood `N(x)`
and a constant `C` such that every `V ∈ ∂F(y)`, `y ∈ N(x)`, is nonsingular with
`‖V⁻¹‖ ≤ C`. -/
theorem prop_3_1 {n : ℕ}
    (F : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) (hF : LocallyLipschitz F)
    (x : EuclideanSpace ℝ (Fin n)) (hns : ∀ V ∈ NonsmoothNewton.Shared.clarkeJac F x, IsUnit V) :
    ∃ N ∈ 𝓝 x, ∃ C : ℝ, ∀ y ∈ N, ∀ V ∈ NonsmoothNewton.Shared.clarkeJac F y,
      ∃ W : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n),
        V.comp W = ContinuousLinearMap.id ℝ _ ∧ W.comp V = ContinuousLinearMap.id ℝ _ ∧
        ‖W‖ ≤ C := by sorry

end NonsmoothNewton.Local

Source

Qi, Sun, A nonsmooth version of Newton's method, Math. Programming 58 (1993), p. 359, Proposition 3.1 (standing assumption p. 358)

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, and linear maps carry the corresponding operator norm. $F : \mathbb{R}^n \to \mathbb{R}^n$ is locally Lipschitz: every point has a neighbourhood on which $F$ is Lipschitz. $x \in \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.

Hypothesis. Every $V \in \mathcal{J}_F(x)$ is invertible as a linear map of $\mathbb{R}^n$ .

Conclusion. There exist a neighbourhood $N$ of $x$ and a real constant $C$ with the following property. For every $y \in N$ and every $V \in \mathcal{J}_F(y)$ there is a linear map $W : \mathbb{R}^n \to \mathbb{R}^n$ with

V W = \mathrm{id}, \qquad W V = \mathrm{id}, \qquad \|W\| \le C .

In other words, every such $V$ is invertible, and its inverse $W = V^{-1}$ has operator norm at most $C$ . The constant $C$ is uniform over all $y \in N$ and all $V \in \mathcal{J}_F(y)$ .

Degenerate cases.

Empty $\mathcal{J}_F(x)$ . The hypothesis is vacuous, and the theorem still asserts the uniform-inverse property near $x$ .
Empty $\mathcal{J}_F(y)$ . If $\mathcal{J}_F(y)$ is empty for all $y$ near $x$ , the conclusion is vacuous.
$n = 0$ . $\mathbb{R}^0$ is a single point, and the only linear map is $0 = \mathrm{id}$ . It is invertible with norm $0$ , so the statement holds trivially (for example with $C = 0$ ).

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

Proposition 3.1 — uniform bound on ∥V−1∥\|V^{-1}\|∥V−1∥ near a point where ∂F\partial F∂F is nonsingular

Proposition 3.1 — uniform bound on $\|V^{-1}\|$ near a point where $\partial F$ is nonsingular