Theorem 2.3 (i)⇔(iv)⇔(v) — characterizations of semismoothness

Proved

NonsmoothNewton.Local.theorem_2_3

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

nonsmooth-analysisp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1semismooth

Let $E$ , $G$ be finite-dimensional real normed spaces, $F : E \to G$ locally Lipschitz, and $x \in E$ . Write $D_F$ for the set of points where $F$ is differentiable. The following statements are equivalent:

(i) $F$ is semismooth at $x$ ;
(iv) $F'(x;h)$ exists for every $h$ , and for $V \in \partial F(x+h)$ , $h \to 0$ ,

Vh - F'(x;h) = o(\|h\|); \tag{2.8}

(v) $F'(x;h)$ exists for every $h$ , and

\lim_{\substack{x+h\in D_F \\ h\to 0}} \frac{F'(x+h;h) - F'(x;h)}{\|h\|} = 0. \tag{2.9}

Condition (2.8) is the form of semismoothness used in the local convergence proof of the nonsmooth Newton method (Theorem 3.2), and (2.9) is the form used to check semismoothness of concrete maps.

Formalization Note The statement is the conjunction of (i) ⇔ (iv) and (i) ⇔ (v); the paper's parts (ii) and (iii) (uniform convergence of the limits in (2.7) and (2.5) over unit directions) are not included. Both $o(\cdot)$ statements are pinned to their $\varepsilon$ – $\delta$ content: for every $\varepsilon > 0$ there is $\delta > 0$ such that $\|Vh - F'(x;h)\| \le \varepsilon\|h\|$ for all $\|h\| < \delta$ and $V \in \partial F(x+h)$ , respectively $\|JF(x+h)h - F'(x;h)\| \le \varepsilon \|h\|$ for all $\|h\| < \delta$ with $x + h \in D_F$ . At a point of differentiability $F'(x+h;h)$ equals $JF(x+h)h$ , which is how (v) is written. Existence of $F'(x;\cdot)$ , which (2.8) and (2.9) presuppose, is part of conditions (iv) and (v).

Preamble

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

Formal statement

namespace NonsmoothNewton.Local

/-- Qi–Sun (1993), Theorem 2.3, p. 356, parts (i) ⇔ (iv) ⇔ (v). For locally Lipschitz `F`:
(i) `F` is semismooth at `x`;
(iv) `F'(x; ·)` exists and `V h - F'(x; h) = o(‖h‖)` for `V ∈ ∂F(x + h)`, `h → 0` (2.8);
(v) `F'(x; ·)` exists and `(F'(x + h; h) - F'(x; h)) / ‖h‖ → 0` as `h → 0` with
`x + h ∈ D_F` (2.9), where at a point of differentiability `F'(x + h; h) = JF(x + h) h`. -/
theorem theorem_2_3 {E G : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] [NormedAddCommGroup G] [NormedSpace ℝ G] [FiniteDimensional ℝ G]
    (F : E → G) (hF : LocallyLipschitz F) (x : E) :
    (SemismoothAt F x ↔
      ((∀ h : E, ∃ d : G, HasDirDerivAt F x h d) ∧
        ∀ ε > 0, ∃ δ > 0, ∀ h : E, ‖h‖ < δ → ∀ V ∈ NonsmoothNewton.Shared.clarkeJac F (x + h),
          ‖V h - dirDeriv F x h‖ ≤ ε * ‖h‖)) ∧
    (SemismoothAt F x ↔
      ((∀ h : E, ∃ d : G, HasDirDerivAt F x h d) ∧
        ∀ ε > 0, ∃ δ > 0, ∀ h : E, ‖h‖ < δ → DifferentiableAt ℝ F (x + h) →
          ‖fderiv ℝ F (x + h) h - dirDeriv F x h‖ ≤ ε * ‖h‖)) := by sorry

end NonsmoothNewton.Local

Source

Qi, Sun, A nonsmooth version of Newton's method, Math. Programming 58 (1993), p. 356, Theorem 2.3 (i), (iv), (v); Eqs. (2.8), (2.9)

Read-back

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

Setting. $E$ and $G$ are finite-dimensional real normed spaces. $F : E \to G$ is locally Lipschitz on all of $E$ , and $x \in E$ . $\mathcal{J}_F(y)$ is the set of continuous linear maps $E \to G$ given by the external definition clarkeJac, which is not shown here.

"Semismooth at $x$ " means both of the following:

$F$ is $K$ -Lipschitz on some neighbourhood of $x$ for some $K \ge 0$ .
For every $h \in E$ there is $L_h \in G$ 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')$ .

$F'(x;h)$ denotes the value assigned to the one-sided limit $\lim_{t \downarrow 0} t^{-1}(F(x+th) - F(x))$ . In both right-hand sides below it is a genuine limit, because existence for every $h$ is stated as a conjunct.

First claim. $F$ is semismooth at $x$ if and only if:

(a) for every $h \in E$ the one-sided directional derivative $F'(x;h)$ exists, and
(b) for every $\varepsilon > 0$ there is a $\delta > 0$ such that for all $h$ with $\|h\| < \delta$ and all $V \in \mathcal{J}_F(x+h)$ ,

\|V h - F'(x;h)\| \le \varepsilon \|h\| .

Second claim. $F$ is semismooth at $x$ if and only if:

(a) for every $h \in E$ the one-sided directional derivative $F'(x;h)$ exists, and
(b′) for every $\varepsilon > 0$ there is a $\delta > 0$ such that for all $h$ with $\|h\| < \delta$ at which $F$ is Fréchet differentiable at $x + h$ , with Fréchet derivative $DF(x+h)$ ,

\|DF(x+h)\,h - F'(x;h)\| \le \varepsilon \|h\| .

In (b′), points $x+h$ where $F$ is not differentiable impose no condition. The set $\mathcal{J}_F$ does not appear in (b′).

Degenerate cases.

$h = 0$ . Both sides of the inequalities in (b) and (b′) are $0$ .
Empty $\mathcal{J}_F$ . If $\mathcal{J}_F(x+h)$ is empty for all small $h$ , then condition (b) is vacuous.
Zero spaces. If $E$ is the zero space, only $h = 0$ exists. If $G$ is the zero space, all vectors in $G$ are $0$ . In either case (a), (b) and (b′) hold trivially, and each equivalence reduces to whether semismoothness holds. That in turn depends on the unseen sets $\mathcal{J}_F$ only through the limit condition, which is satisfied with $L_h = 0$ in these cases.

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