Corollary 2.5 — a strong Fréchet derivative implies semismoothness

Proved

NonsmoothNewton.Local.cor_2_5

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$ . Suppose $F$ has a strong Fréchet derivative $F'(x)$ at $x$ , i.e.

\lim_{\substack{y \to x \\ z \to x}} \frac{F(z) - F(y) - F'(x)(z-y)}{\|z-y\|} = 0 .

Then $F$ is semismooth at $x$ .

This shows that the class of semismooth maps contains every map that is strictly differentiable at the point, in particular every continuously differentiable map.

Formalization Note The paper's display (2.16) prints $F(x)$ in the numerator where $F(z)$ is meant; as printed the limit fails for every nonconstant $F$ . The proof of the corollary (taking $z = y + th$ ) and the cited definition of Ortega–Rheinboldt use $F(z)$ , and the corrected form is stated. It is Mathlib's HasStrictFDerivAt, which reads the quotient as $\|F(z)-F(y)-F'(x)(z-y)\| = o(\|z-y\|)$ as $(y,z) \to (x,x)$ .

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), Corollary 2.5, p. 358. If the locally Lipschitz map `F` has a strong
Fréchet derivative `F'` at `x` (Mathlib's `HasStrictFDerivAt`: the corrected (2.16),
`(F z - F y - F'(z - y)) / ‖z - y‖ → 0` as `y, z → x`), then `F` is semismooth at `x`. -/
theorem cor_2_5 {E G : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    [NormedAddCommGroup G] [NormedSpace ℝ G] [FiniteDimensional ℝ G]
    (F : E → G) (hF : LocallyLipschitz F) (x : E) (F' : E →L[ℝ] G)
    (hstrong : HasStrictFDerivAt F F' x) :
    SemismoothAt F x := by sorry

end NonsmoothNewton.Local

Source

Qi, Sun, A nonsmooth version of Newton's method, Math. Programming 58 (1993), p. 358, Corollary 2.5 (definition (2.16), same page)

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$ . $x \in E$ , and $F' : E \to G$ is a continuous linear map.

Hypothesis. $F$ has strict (strong) Fréchet derivative $F'$ at $x$ :

F(z) - F(y) - F'(z - y) = o(\|z - y\|) \quad \text{as } (y, z) \to (x, x),

with $y$ and $z$ varying independently.

Conclusion. $F$ is semismooth at $x$ , which means both of the following:

There are $K \ge 0$ and a neighbourhood $U$ of $x$ on which $F$ is $K$ -Lipschitz.
For every direction $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

for all reals $0 < t < \delta$ , all $h'$ with $\|h' - h\| < \delta$ , and all $V \in \mathcal{J}_F(x + t h')$ .

Here $\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. The conclusion does not state that $L_h$ equals $F' h$ .

Degenerate cases.

Empty $\mathcal{J}_F$ . If $\mathcal{J}_F(x + th')$ is empty near $x$ , part 2 is vacuous.
Zero spaces. If $E$ or $G$ is the zero space, both the hypothesis and the conclusion hold trivially: in part 2, $L_h = 0$ works because $h' = 0$ or $G = \{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