Eq. (4.2): the Hessian of $\eta$ off the surface $s + r g(x) = 0$ , where $\nabla\eta$ is smooth

Proved

NonsmoothNewton.AugLagrangian.eta_grad_smooth_off_surface

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

augmented-lagrangiannonsmooth-analysisp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1

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

\nabla^2 \eta(x, s) = \begin{cases} \begin{pmatrix} r \nabla g(x) \nabla g(x)^{\mathsf T} + (s + r g(x)) \nabla^2 g(x) & \nabla g(x) \\ \nabla g(x)^{\mathsf T} & 0 \end{pmatrix}, & s + r g(x) > 0,\\[10pt] \begin{pmatrix} 0 & 0 \\ 0 & -1/r \end{pmatrix}, & s + r g(x) < 0, \end{cases} \tag{4.2}

and $\nabla \eta$ is continuously differentiable in a neighbourhood of every point $(x, s)$ with $s + r g(x) \neq 0$ .

That is, $\nabla\eta$ is smooth except on the surface $s + r g(x) = 0$ ; the remaining work of Theorem 4.1 is semismoothness on that surface.

Formalization Note The Hessian is the Fréchet derivative of the map $(x, s) \mapsto D\eta(x, s)$ . Applied to a direction $(h, \alpha)$ it is stated as the linear functional $(k, \beta) \mapsto (r\, Dg(x)h + \alpha)\, Dg(x)k + (s + r g(x))\, D^2 g(x)(h, k) + Dg(x)h\, \beta$ when $s + r g(x) > 0$ , and $(k, \beta) \mapsto -(\alpha / r)\,\beta$ when $s + r g(x) < 0$ , which is the matrix (4.2) applied to $(h, \alpha)$ and paired with $(k, \beta)$ . "Smooth" is the paper's continuously differentiable (ContDiffAt ℝ 1).

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, Eq. (4.2), p. 364. For `r > 0` and `g ∈ C²`, the Hessian of
`η(x, s) = φ(r, g(x), s)` is, applied to a direction `(h, α)`,
`(r ∇g(x)∇g(x)ᵀ + (s + r g(x)) ∇²g(x)) h + α ∇g(x)` in `x` and `∇g(x)ᵀ h` in `s` where
`s + r g(x) > 0`, and `(0, -α/r)` where `s + r g(x) < 0`; and `∇η` is `C¹` near every point
off the surface `s + r g(x) = 0`. -/
theorem eta_grad_smooth_off_surface {n : ℕ} (r : ℝ) (hr : 0 < r)
    (g : EuclideanSpace ℝ (Fin n) → ℝ) (hg : ContDiff ℝ 2 g) :
    (∀ z : EuclideanSpace ℝ (Fin n) × ℝ, 0 < z.2 + r * g z.1 →
      ∀ v : EuclideanSpace ℝ (Fin n) × ℝ,
        fderiv ℝ (fun w => fderiv ℝ (eta r g) w) z v =
          (r * fderiv ℝ g z.1 v.1 + v.2) • (fderiv ℝ g z.1).comp
              (ContinuousLinearMap.fst ℝ (EuclideanSpace ℝ (Fin n)) ℝ)
            + (z.2 + r * g z.1) • (fderiv ℝ (fun u => fderiv ℝ g u) z.1 v.1).comp
              (ContinuousLinearMap.fst ℝ (EuclideanSpace ℝ (Fin n)) ℝ)
            + fderiv ℝ g z.1 v.1 • ContinuousLinearMap.snd ℝ (EuclideanSpace ℝ (Fin n)) ℝ) ∧
    (∀ z : EuclideanSpace ℝ (Fin n) × ℝ, z.2 + r * g z.1 < 0 →
      ∀ v : EuclideanSpace ℝ (Fin n) × ℝ,
        fderiv ℝ (fun w => fderiv ℝ (eta r g) w) z v =
          (-(v.2 / r)) • ContinuousLinearMap.snd ℝ (EuclideanSpace ℝ (Fin n)) ℝ) ∧
    (∀ z : EuclideanSpace ℝ (Fin n) × ℝ, z.2 + r * g z.1 ≠ 0 →
      ContDiffAt ℝ 1 (fun w => fderiv ℝ (eta r g) w) z) := by sorry

end NonsmoothNewton.AugLagrangian

Source

Qi, Sun, A nonsmooth version of Newton's method, Math. Programming 58 (1993), p. 364, Section 4, Eq. (4.2) and the sentence after it

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.

Consider the map $\Gamma : z \mapsto D\eta(z)$ . It sends each point of $\mathbb{R}^n \times \mathbb{R}$ to a linear functional on $\mathbb{R}^n \times \mathbb{R}$ . Write $D\Gamma(z)\,v$ for the derivative of $\Gamma$ at $z$ applied to a direction $v$ ; this is again a linear functional. Write $D^2 g(x)(h, k)$ for the derivative of $u \mapsto Dg(u)$ at $x$ , applied first to $h$ and then to $k$ .

Conclusion. The statement asserts all three of the following.

At every $z = (x, s)$ with $s + r g(x) > 0$ (strictly), and for every direction $v = (h, \alpha)$ , the functional $D\Gamma(z)\,v$ acts on $(k, \beta) \in \mathbb{R}^n \times \mathbb{R}$ by

\big(D\Gamma(z)\,v\big)(k, \beta) = \big(r\, Dg(x)\,h + \alpha\big)\, Dg(x)\,k + \big(s + r g(x)\big)\, D^2 g(x)(h, k) + \big(Dg(x)\,h\big)\,\beta.

At every $z = (x, s)$ with $s + r g(x) < 0$ (strictly), and for every direction $v = (h, \alpha)$ :

\big(D\Gamma(z)\,v\big)(k, \beta) = -\frac{\alpha}{r}\,\beta.

At every $z = (x, s)$ with $s + r g(x) \ne 0$ , the map $\Gamma$ is continuously differentiable ( $C^1$ ) at $z$ .

Nothing is said about points where $s + r g(x) = 0$ .

Degenerate cases:

By default the derivative of a non-differentiable function is $0$ . The formulas in items 1 and 2 are stated as literal equalities with the value returned under that convention. Item 3 separately asserts that $\Gamma$ is differentiable at the points off the surface.
$n = 0$ . $g$ is a constant $c$ , $Dg = 0$ and $D^2 g = 0$ . Item 1 then says $D\Gamma(z)\,v$ is the functional $(k, \beta) \mapsto 0$ wherever $s + r c > 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

Eq. (4.2): the Hessian of η\etaη off the surface s+rg(x)=0s + r g(x) = 0s+rg(x)=0, where ∇η\nabla\eta∇η is smooth

Eq. (4.2): the Hessian of $\eta$ off the surface $s + r g(x) = 0$ , where $\nabla\eta$ is smooth