Remark (2.17) — first-order expansion $F(x+h)-F(x)-F'(x;h)=o(\|h\|)$ at a semismooth point

Proved

NonsmoothNewton.Local.remark_2_17

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$ .

If $F$ is semismooth at $x$ , then as $h \to 0$

F(x+h) - F(x) - F'(x;h) = o(\|h\|). \tag{2.17}

If $0 < p \le 1$ and $F$ is $p$ -order semismooth at $x$ , then as $h \to 0$

F(x+h) - F(x) - F'(x;h) = O(\|h\|^{1+p}).

Together with (2.8), the expansion (2.17) is what lets the Newton step be compared with the directional derivative at the root in the proof of Theorem 3.2; the second clause gives the order $1+p$ .

Formalization Note The $o(\|h\|)$ is pinned as: for every $\varepsilon > 0$ there is $\delta > 0$ with $\|F(x+h)-F(x)-F'(x;h)\| \le \varepsilon\|h\|$ whenever $\|h\| < \delta$ . The $O(\|h\|^{1+p})$ is pinned as: there are $C$ and $\delta > 0$ with the same norm $\le C\|h\|^{1+p}$ whenever $\|h\| < \delta$ . The Remark is unnumbered in the paper and cited by its equation number.

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), Section 2, Remark, Eq. (2.17), p. 358. For locally Lipschitz `F`:
if `F` is semismooth at `x` then `F(x + h) - F(x) - F'(x; h) = o(‖h‖)`; if `F` is
`p`-order semismooth at `x` (`0 < p ≤ 1`) then `F(x + h) - F(x) - F'(x; h) = O(‖h‖^{1+p})`. -/
theorem remark_2_17 {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 → ∀ ε > 0, ∃ δ > 0, ∀ h : E, ‖h‖ < δ →
        ‖F (x + h) - F x - dirDeriv F x h‖ ≤ ε * ‖h‖) ∧
    (∀ p : ℝ, 0 < p → p ≤ 1 → POrderSemismoothAt p F x →
      ∃ C δ : ℝ, 0 < δ ∧ ∀ h : E, ‖h‖ < δ →
        ‖F (x + h) - F x - dirDeriv F x h‖ ≤ C * ‖h‖ ^ (1 + p)) := by sorry

end NonsmoothNewton.Local

Source

Qi, Sun, A nonsmooth version of Newton's method, Math. Programming 58 (1993), p. 358, Section 2, Remark, Eq. (2.17)

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.

$F'(x;h)$ is the value assigned to the one-sided limit $\lim_{t \downarrow 0} t^{-1}(F(x+th) - F(x))$ . This value is the true limit when the limit exists, and an unspecified fixed element of $G$ otherwise. The statement contains no separate hypothesis that the limit exists.

The semismoothness notions used are:

Semismooth at $x$ . $F$ is $K$ -Lipschitz near $x$ for some $K \ge 0$ , and for every $h$ there is $L_h$ with $\|V h' - L_h\| < \varepsilon$ whenever $0 < t < \delta$ , $\|h' - h\| < \delta$ and $V \in \mathcal{J}_F(x + t h')$ (with $\delta$ depending on $\varepsilon$ ).
$p$ -order semismooth at $x$ . $F$ is semismooth at $x$ , and there are real $C$ and $\delta > 0$ with $\|Vh - d\| \le C\|h\|^{1+p}$ for all $\|h\| < \delta$ , all $V \in \mathcal{J}_F(x+h)$ , and every $d$ that is the one-sided directional derivative of $F$ at $x$ in direction $h$ .

Conclusion. Both of the following hold.

Semismooth case. If $F$ is semismooth at $x$ , then for every $\varepsilon > 0$ there is a $\delta > 0$ such that for all $h$ with $\|h\| < \delta$ ,

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

$p$ -order case. For every real $p$ with $0 < p \le 1$ : if $F$ is $p$ -order semismooth at $x$ , then there are real numbers $C$ and $\delta > 0$ such that for all $h$ with $\|h\| < \delta$ ,

\|F(x+h) - F(x) - F'(x;h)\| \le C \|h\|^{1+p} .

Degenerate cases.

$h = 0$ . $F'(x;0) = 0$ , so both bounds read $0 \le 0$ .
Junk values. For any direction in which the one-sided limit might fail to exist, the bounds are asserted for the unspecified junk value of $F'(x;h)$ .
Zero spaces. If $E$ or $G$ is the zero space, both conclusions hold 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

Remark (2.17) — first-order expansion F(x+h)−F(x)−F′(x;h)=o(∥h∥)F(x+h)-F(x)-F'(x;h)=o(\|h\|)F(x+h)−F(x)−F′(x;h)=o(∥h∥) at a semismooth point

Remark (2.17) — first-order expansion $F(x+h)-F(x)-F'(x;h)=o(\|h\|)$ at a semismooth point