Prove2Me

Lemma 2.2 — F′(x;⋅)F'(x;\cdot) is Lipschitz and F′(x;h)=VhF'(x;h)=Vh for some V∈∂F(x)V\in\partial F(x)

Proved
NonsmoothNewton.Local.lemma_2_2

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

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

Let EE, GG be finite-dimensional real normed spaces and F:E→GF : E \to G locally Lipschitz, and suppose the one-sided directional derivative F′(x;h)F'(x;h) exists for every h∈Eh \in E. Then

  1. the map h↦F′(x;h)h \mapsto F'(x;h) is Lipschitz: there is K≥0K \ge 0 with ∥F′(x;h)−F′(x;h′)∥≤K∥h−h′∥\|F'(x;h) - F'(x;h')\| \le K\|h - h'\| for all h,h′h, h';
  2. for every hh there is V∈∂F(x)V \in \partial F(x) with
F′(x;h)=Vh.F'(x;h) = V h .

Part (ii) says the directional derivative is realised by an element of the generalized Jacobian, direction by direction; together with (i) it is used to pass between the characterizations of semismoothness in Theorem 2.3.

Formalization Note The paper's Rn→Rm\mathbb R^n \to \mathbb R^m is generalised to finite-dimensional normed spaces; the Lipschitz constant is existential.

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), Lemma 2.2, p. 356. If `F` is locally Lipschitz and `F'(x; h)` exists for
every `h`, then (i) `h ↦ F'(x; h)` is Lipschitz and (ii) for every `h` there is
`V ∈ ∂F(x)` with `F'(x; h) = V h`. -/
theorem lemma_2_2 {E G : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    [NormedAddCommGroup G] [NormedSpace ℝ G] [FiniteDimensional ℝ G]
    (F : E → G) (hF : LocallyLipschitz F) (x : E)
    (hdir : ∀ h : E, ∃ d : G, HasDirDerivAt F x h d) :
    (∃ K : NNReal, LipschitzWith K (fun h : E => dirDeriv F x h)) ∧
    ∀ h : E, ∃ V ∈ NonsmoothNewton.Shared.clarkeJac F x, dirDeriv F x h = V h := by sorry

end NonsmoothNewton.Local
Source
Qi, Sun, A nonsmooth version of Newton's method, Math. Programming 58 (1993), p. 356, Lemma 2.2
Read-back

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

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

Hypothesis. For every direction h∈Eh \in E the one-sided directional derivative exists:

F′(x;h):=lim⁡t→0, t>01t(F(x+th)−F(x)).F'(x;h) := \lim_{t \to 0,\ t > 0} \frac{1}{t}\bigl(F(x+th) - F(x)\bigr).

Because of this hypothesis, the value F′(x;h)F'(x;h) used below is this genuine limit for every hh.

Conclusion. Both of the following hold.

  1. Lipschitz in the direction. There is a constant K≥0K \ge 0 such that the map h↦F′(x;h)h \mapsto F'(x;h) is KK-Lipschitz on the whole of EE:
∥F′(x;h1)−F′(x;h2)∥≤K∥h1−h2∥for all h1,h2∈E.\|F'(x;h_1) - F'(x;h_2)\| \le K \|h_1 - h_2\| \quad \text{for all } h_1, h_2 \in E.
  1. Representation by an element of JF(x)\mathcal{J}_F(x). For every h∈Eh \in E there exists V∈JF(x)V \in \mathcal{J}_F(x), possibly depending on hh, with
F′(x;h)=Vh.F'(x;h) = V h .

In particular, this asserts that JF(x)\mathcal{J}_F(x) is nonempty whenever EE is nonempty, which is always the case.

Degenerate cases.

  • For h=0h = 0, part 2 reads 0=V00 = V0, which holds for any VV. It still requires JF(x)≠∅\mathcal{J}_F(x) \neq \emptyset.
  • If EE is the zero space, only h=0h = 0 occurs. Part 1 is trivial, and part 2 again reduces to the nonemptiness of JF(x)\mathcal{J}_F(x).
  • If GG is the zero space, all derivative values are 00, and part 2 again reduces to the nonemptiness of JF(x)\mathcal{J}_F(x).
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