Proof of Theorem 4.1: $\nabla\eta$ is semismooth at every point of the surface $s + r g(x) = 0$

Proved

NonsmoothNewton.AugLagrangian.eta_grad_semismooth_on_surface

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

augmented-lagrangianp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1semismooth

Let $r > 0$ , let $g : \mathbb{R}^n \to \mathbb{R}$ be of class $C^2$ , and let $\eta(x, s) = \phi(r, g(x), s)$ . If $(\bar x, \bar s)$ satisfies

\bar s + r g(\bar x) = 0, \tag{4.3}

then $\nabla \eta$ , as a map of $(x, s) \in \mathbb{R}^{n+1}$ , is semismooth at $(\bar x, \bar s)$ : it is locally Lipschitz there and, for every $(h, \alpha) \in \mathbb{R}^{n+1}$ , the limit

\lim_{\substack{h' \to h,\ \alpha' \to \alpha \\ t \downarrow 0}} \Big\{ V \begin{pmatrix} h' \\ \alpha' \end{pmatrix} : V \in \partial \nabla \eta(\bar x + t h', \bar s + t \alpha') \Big\} \tag{4.4}

exists.

This is the nonsmooth heart of Theorem 4.1: on the surface where the two formulas for $\phi$ meet, $\nabla\eta$ is not differentiable, yet it is semismooth, which is what the nonsmooth Newton method requires.

Formalization Note $\nabla\eta$ is the Fréchet derivative map $(x,s) \mapsto D\eta(x,s)$ , valued in linear functionals on $\mathbb{R}^n \times \mathbb{R}$ ; semismoothness is invariant under the Riesz isometry between functionals and gradient vectors and under the choice of equivalent norm on $\mathbb{R}^n \times \mathbb{R}$ (Mathlib's product carries the sup norm). The semismoothness is joint in $(x, s)$ .

Preamble

import Mathlib
import Definitions.Def_NonsmoothNewton_Shared_clarkeJac
import Definitions.Def_NonsmoothNewton_AugLagrangian_SemismoothAt
import Definitions.Def_NonsmoothNewton_AugLagrangian_augLagrangian
open Filter Topology

Formal statement

namespace NonsmoothNewton.AugLagrangian

/-- Qi–Sun (1993), Section 4, proof of Theorem 4.1, pp. 364–365. For `r > 0` and `g ∈ C²`, the
gradient of `η(x, s) = φ(r, g(x), s)` is semismooth (jointly in `(x, s)`) at every point
`(x̄, s̄)` of the surface `s̄ + r g(x̄) = 0`. -/
theorem eta_grad_semismooth_on_surface {n : ℕ} (r : ℝ) (hr : 0 < r)
    (g : EuclideanSpace ℝ (Fin n) → ℝ) (hg : ContDiff ℝ 2 g)
    (xbar : EuclideanSpace ℝ (Fin n)) (sbar : ℝ) (h43 : sbar + r * g xbar = 0) :
    SemismoothAt (fun w => fderiv ℝ (eta r g) w) (xbar, sbar) := by sorry

end NonsmoothNewton.AugLagrangian

Source

Qi, Sun, A nonsmooth version of Newton's method, Math. Programming 58 (1993), pp. 364–365, Section 4, proof of Theorem 4.1, Eqs. (4.3)–(4.4) and the conclusion on p. 365

Read-back

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

Setting. Let $n \in \mathbb{N}$ , let $r$ be a real number with $r > 0$ , and let $g : \mathbb{R}^n \to \mathbb{R}$ be $C^2$ , with $\mathbb{R}^n$ Euclidean. Let

\eta(x, s) = \varphi(r, g(x), s),

where $\varphi(r, a, s) = s a + \frac{r}{2} a^2$ if $s + r a \ge 0$ , and $\varphi(r, a, s) = -\frac{1}{2r} s^2$ otherwise.

Let $\Gamma : z \mapsto D\eta(z)$ be the map sending each point $z \in \mathbb{R}^n \times \mathbb{R}$ to the derivative of $\eta$ at $z$ . This is a linear functional on $\mathbb{R}^n \times \mathbb{R}$ , measured in operator norm; by convention it is $0$ wherever $\eta$ is not differentiable. The space $\mathbb{R}^n \times \mathbb{R}$ carries the norm $\|(h, \alpha)\| = \max(\|h\|_2, |\alpha|)$ .

Let $(\bar{x}, \bar{s})$ be any point with

\bar{s} + r\, g(\bar{x}) = 0.

Conclusion. $\Gamma$ is "semismooth at $(\bar{x}, \bar{s})$ " in the sense defined in this bundle. Unfolded, this means both of the following hold.

There are $K \ge 0$ and a neighbourhood $U$ of $(\bar{x}, \bar{s})$ on which $\Gamma$ is $K$ -Lipschitz.
For every direction $v \in \mathbb{R}^n \times \mathbb{R}$ there is a linear functional $\Lambda$ on $\mathbb{R}^n \times \mathbb{R}$ with the following property. For every $\varepsilon > 0$ there is a $\delta > 0$ such that

\|V v' - \Lambda\| < \varepsilon

for every $t$ with $0 < t < \delta$ , every $v'$ with $\|v' - v\| < \delta$ , and every $V \in \partial\Gamma\big((\bar{x}, \bar{s}) + t v'\big)$ .

Here $\partial\Gamma(y)$ is the set given by the imported definition clarkeJac applied to $\Gamma$ at $y$ . That definition is not included in the code given here, so its contents cannot be spelled out. The code only uses that each $V$ in it can be applied to $v'$ to give a linear functional $V v'$ .

Degenerate cases:

If the sets $\partial\Gamma$ are empty near $(\bar{x}, \bar{s})$ along a direction $v$ , condition 2 holds for that $v$ with any $\Lambda$ , and the conclusion reduces to condition 1.
$n = 0$ . $g$ is a constant $c$ , and the hypothesis fixes $\bar{s} = -rc$ .
The hypothesis $r > 0$ rules out the case $\frac{1}{2r}$ with $r = 0$ .

Human review

Endorsed by Shuze Chen · Sep 28, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 28, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Proof of Theorem 4.1: ∇η\nabla\eta∇η is semismooth at every point of the surface s+rg(x)=0s + r g(x) = 0s+rg(x)=0

Proof of Theorem 4.1: $\nabla\eta$ is semismooth at every point of the surface $s + r g(x) = 0$