Proof of Theorem 4.1: $\eta \in C^1$ , the formula for $\nabla\eta$ , and $\nabla\eta$ locally Lipschitz

Proved

NonsmoothNewton.AugLagrangian.eta_C1_grad_locLip

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$ and let $g : \mathbb{R}^n \to \mathbb{R}$ be of class $C^2$ . Put $\eta(x, s) = \phi(r, g(x), s)$ , i.e.

\eta(x,s) = \begin{cases} s\, g(x) + \tfrac12 r g(x)^2, & s + r g(x) \ge 0,\\ -\tfrac{1}{2r} s^2, & s + r g(x) \le 0.\end{cases}

Then:

$\eta$ is continuously differentiable on $\mathbb{R}^n \times \mathbb{R}$ ;
its gradient is

\nabla \eta(x, s) = \begin{cases} \begin{pmatrix} (s + r g(x)) \nabla g(x) \\ g(x) \end{pmatrix}, & s + r g(x) \ge 0,\\[6pt] \begin{pmatrix} 0 \\ -s/r \end{pmatrix}, & s + r g(x) \le 0; \end{cases}

$\nabla \eta$ is locally Lipschitz.

This is the first step of the proof of Theorem 4.1: it establishes that each inequality term of the augmented Lagrangian is $C^1$ and that its gradient is regular enough (locally Lipschitz) for semismoothness to make sense.

Formalization Note The gradient is represented by the Fréchet derivative, a continuous linear functional on $\mathbb{R}^n \times \mathbb{R}$ : in the first case $(h, \alpha) \mapsto (s + r g(x))\, Dg(x) h + g(x)\, \alpha$ , in the second $(h, \alpha) \mapsto -(s/r)\, \alpha$ . It corresponds to the gradient vector through the Riesz isometry.

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. 363–364. For `r > 0` and `g ∈ C²`,
`η(x, s) = φ(r, g(x), s)` is `C¹`, its gradient is
`∇η(x, s) = ((s + r g(x)) ∇g(x), g(x))` if `s + r g(x) ≥ 0` and `(0, -s/r)` if
`s + r g(x) ≤ 0` (here as the Fréchet derivative, a linear functional on `ℝⁿ × ℝ`),
and `∇η` is locally Lipschitz. -/
theorem eta_C1_grad_locLip {n : ℕ} (r : ℝ) (hr : 0 < r) (g : EuclideanSpace ℝ (Fin n) → ℝ)
    (hg : ContDiff ℝ 2 g) :
    ContDiff ℝ 1 (eta r g) ∧
    (∀ z : EuclideanSpace ℝ (Fin n) × ℝ, 0 ≤ z.2 + r * g z.1 →
      fderiv ℝ (eta r g) z =
        (z.2 + r * g z.1) • (fderiv ℝ g z.1).comp
            (ContinuousLinearMap.fst ℝ (EuclideanSpace ℝ (Fin n)) ℝ)
          + g z.1 • ContinuousLinearMap.snd ℝ (EuclideanSpace ℝ (Fin n)) ℝ) ∧
    (∀ z : EuclideanSpace ℝ (Fin n) × ℝ, z.2 + r * g z.1 ≤ 0 →
      fderiv ℝ (eta r g) z =
        (-(z.2 / r)) • ContinuousLinearMap.snd ℝ (EuclideanSpace ℝ (Fin n)) ℝ) ∧
    LocallyLipschitz (fun z => fderiv ℝ (eta r g) z) := by sorry

end NonsmoothNewton.AugLagrangian

Source

Qi, Sun, A nonsmooth version of Newton's method, Math. Programming 58 (1993), pp. 363–364, Section 4, proof of Theorem 4.1 (display of ∇η 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 twice continuously differentiable ( $C^2$ ) on all of $\mathbb{R}^n$ , which has its Euclidean structure. 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. The domain of $\eta$ is $\mathbb{R}^n \times \mathbb{R}$ . Write $D\eta(x, s)$ for its derivative, a linear map from $\mathbb{R}^n \times \mathbb{R}$ to $\mathbb{R}$ , and $Dg(x)$ for the derivative of $g$ .

Conclusion. The statement asserts all four of the following.

$\eta$ is continuously differentiable ( $C^1$ ) on all of $\mathbb{R}^n \times \mathbb{R}$ .
At every $(x, s)$ with $s + r g(x) \ge 0$ , and for every direction $(h, \alpha) \in \mathbb{R}^n \times \mathbb{R}$ :

D\eta(x, s)(h, \alpha) = \big(s + r g(x)\big)\, Dg(x)\,h + g(x)\,\alpha.

At every $(x, s)$ with $s + r g(x) \le 0$ , and for every direction $(h, \alpha)$ :

D\eta(x, s)(h, \alpha) = -\frac{s}{r}\,\alpha.

The map $z \mapsto D\eta(z)$ is locally Lipschitz. Here $D\eta(z)$ is viewed as a linear functional, measured in operator norm. Every point of $\mathbb{R}^n \times \mathbb{R}$ has a neighbourhood on which this map is Lipschitz with some constant.

Items 2 and 3 both use non-strict inequalities. At points with $s + r g(x) = 0$ both apply, so the statement also asserts that the two formulas give the same functional there.

Degenerate cases:

The hypothesis $r > 0$ rules out the case $\frac{1}{2r}$ with $r = 0$ .
By default the derivative of a non-differentiable function is taken to be $0$ . That convention never applies here, because item 1 asserts that $\eta$ is differentiable everywhere.
$n = 0$ . $g$ is a constant $c$ , and $Dg = 0$ . The formulas become $D\eta(x, s)(h, \alpha) = c\,\alpha$ where $s + r c \ge 0$ , and $-\frac{s}{r}\alpha$ where $s + r c \le 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: η∈C1\eta \in C^1η∈C1, the formula for ∇η\nabla\eta∇η, and ∇η\nabla\eta∇η locally Lipschitz

Proof of Theorem 4.1: $\eta \in C^1$ , the formula for $\nabla\eta$ , and $\nabla\eta$ locally Lipschitz