Proposition 2.1 — the limit of $Vh$ over $V\in\partial F(x+th)$ is the directional derivative

Proved

NonsmoothNewton.Local.prop_2_1

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

directional-derivativenonsmooth-analysisp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $E$ , $G$ be finite-dimensional real normed spaces and $F : E \to G$ locally Lipschitz. Fix $x, h \in E$ and suppose the limit

L = \lim_{\substack{V \in \partial F(x+th) \\ t \downarrow 0}} \{V h\} \tag{2.3}

exists, i.e. for every $\varepsilon > 0$ there is $\delta > 0$ with $\|Vh - L\| < \varepsilon$ whenever $0 < t < \delta$ and $V \in \partial F(x+th)$ . Then the classic directional derivative exists and equals this limit:

F'(x;h) = \lim_{t\downarrow 0}\frac{F(x+th)-F(x)}{t} = L .

This identifies the directional derivative of a semismooth map with a limit of generalized-Jacobian actions, which is the bridge between the definition of semismoothness and its characterizations.

Formalization Note The paper assumes (2.3) for every $h$ and concludes (2.4)–(2.5) for every $h$ ; the statement here is the same assertion for each fixed direction $h$ separately (the proof in the paper is direction by direction). The paper's $\mathbb R^n \to \mathbb R^m$ is generalised to finite-dimensional normed spaces; Section 2's standing assumption "F locally Lipschitzian" is a hypothesis.

Preamble

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

Formal statement

namespace NonsmoothNewton.Local

/-- Qi–Sun (1993), Proposition 2.1, p. 355. If `F` is locally Lipschitz and, for the direction
`h`, the limit (2.3) `L = lim_{V ∈ ∂F(x + t h), t ↓ 0} V h` exists, then the one-sided
directional derivative `F'(x; h)` (2.4) exists and equals `L` (2.5). -/
theorem prop_2_1 {E G : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    [NormedAddCommGroup G] [NormedSpace ℝ G] [FiniteDimensional ℝ G]
    (F : E → G) (hF : LocallyLipschitz F) (x h : E) (L : G)
    (hL : ∀ ε > 0, ∃ δ > 0, ∀ t : ℝ, 0 < t → t < δ →
      ∀ V ∈ NonsmoothNewton.Shared.clarkeJac F (x + t • h), ‖V h - L‖ < ε) :
    HasDirDerivAt F x h L := by sorry

end NonsmoothNewton.Local

Source

Qi, Sun, A nonsmooth version of Newton's method, Math. Programming 58 (1993), p. 355, Proposition 2.1 (with assumption (2.3), p. 354)

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: every point of $E$ has a neighbourhood on which $F$ is Lipschitz with some constant. Also fixed are $x, h \in E$ and $L \in G$ . $\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.

Hypothesis. For every $\varepsilon > 0$ there is a $\delta > 0$ such that, for every real $t$ with $0 < t < \delta$ and every $V \in \mathcal{J}_F(x + t h)$ ,

\|V h - L\| < \varepsilon .

Only the fixed direction $h$ is used here; directions near $h$ are not involved.

Conclusion. The one-sided directional derivative of $F$ at $x$ in direction $h$ exists and equals $L$ :

\lim_{t \to 0,\ t > 0} \frac{1}{t}\bigl(F(x + t h) - F(x)\bigr) = L .

Degenerate cases.

$h = 0$ . Then $Vh = 0$ , so the hypothesis forces $\|L\| < \varepsilon$ for all $\varepsilon$ , i.e. $L = 0$ . The conclusion then says that the limit is $0$ , which is automatically true.
Empty $\mathcal{J}_F$ . If $\mathcal{J}_F(x + t h)$ is empty for all small $t > 0$ , the hypothesis holds for every $L \in G$ . The theorem would then assert that the limit equals every $L$ at once, which is possible only if $G$ is the zero space.
Zero spaces. If $E$ is the zero space, only $h = 0$ is possible. If $G$ is the zero space, the conclusion is automatic.

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 2.1 — the limit of VhVhVh over V∈∂F(x+th)V\in\partial F(x+th)V∈∂F(x+th) is the directional derivative

Proposition 2.1 — the limit of $Vh$ over $V\in\partial F(x+th)$ is the directional derivative