Prove2Me

The gradient ∇η\nabla\eta of the augmented-Lagrangian inequality term is locally Lipschitz

Proved
NonsmoothNewton.AugLagrangian.eta_fderiv_locallyLipschitz

by WillR · Sep 29, 2026 · Mathlib 0df444a (Lean v4.33.1)

augmented-lagrangiancalculusnonsmooth-analysissource-faithful-child

Let r>0r>0 and g:Rn→Rg:\mathbb{R}^n\to\mathbb{R} be C2C^2, and assume η(x,s)=ϕ(r,g(x),s)\eta(x,s)=\phi(r,g(x),s) is C1C^1. Then the map (x,s)↦Dη(x,s)(x,s)\mapsto D\eta(x,s), valued in the continuous linear functionals on Rn×R\mathbb{R}^n\times\mathbb{R} and measured in operator norm, is locally Lipschitz on Rn×R\mathbb{R}^n\times\mathbb{R}. On the two open regions separated by the surface s+rg(x)=0s+rg(x)=0 this map equals the two smooth expressions ((s+rg(x))Dg(x), g(x))((s+rg(x))Dg(x),\,g(x)) and (0, −sr)(0,\,-\frac sr); these agree on the surface because g(x)=−s/rg(x)=-s/r there, and both are smooth there because DgDg is continuous. This is the local Lipschitz continuity of ∇η\nabla\eta asserted in item 3 of Theorem 4.1, the regularity that makes the semismooth Newton method applicable.

Formal statement
import Mathlib
import Definitions.Def_NonsmoothNewton_Shared_clarkeJac
import Definitions.Def_NonsmoothNewton_AugLagrangian_SemismoothAt
import Definitions.Def_NonsmoothNewton_AugLagrangian_augLagrangian

namespace NonsmoothNewton.AugLagrangian

/-- Child of `eta_C1_grad_locLip`, third step of Qi-Sun (1993), Section 4, proof of Theorem 4.1,
pp. 363-364: $\nabla\eta$ is locally Lipschitz (item 3 of the theorem, the sentence following the
display of the gradient).

The gradient is viewed as a linear functional and bounded in operator norm. Since $g$ is $C^2$,
$\nabla g=fderiv\ \mathbb{R}\ g$ is $C^1$ and therefore locally Lipschitz, and the gradient of $\eta$
differs from the continuous function $(x,s)\mapsto g(x)$ by the term $(s+rg(x))\cdot\Psi$ whose
factor $\Psi$ is bounded on bounded sets. -/
theorem eta_fderiv_locallyLipschitz {n : ℕ} (r : ℝ) (hr : 0 < r)
    (g : EuclideanSpace ℝ (Fin n) → ℝ) (hg : ContDiff ℝ 2 g)
    (hη : ContDiff ℝ 1 (eta r g)) :
    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, the sentence following the display of ∇η\nabla\eta (item 3 of the theorem).

View graph