Coordinatewise Hessian Bound from Gradient Lipschitzness

This declaration gives a coordinatewise weak-Hessian estimate and is listed as partially related to the Key moment-map Hessian bound, Theorem 2.5 of Letwin (arXiv:2607.24164v1).

Let $n$ be a natural number, let $u : \mathbb{R}^n \to \mathbb{R}$ be represented by EuclideanSpace ℝ (Fin n), and let $G$ be a nonnegative real number represented by NNReal. Assume that the gradient map $\nabla u$ is $G$-Lipschitz with respect to the Euclidean norm. Then, for every point $x \in \operatorname{EuclideanSpace}(\mathbb{R},\operatorname{Fin}(n))$ and every pair of coordinate indices $i,j \in \operatorname{Fin}(n)$, the corresponding entry of hessianMatrix u x satisfies

Here the norm on the real-valued Hessian entry is the usual absolute-value norm, and $G$ on the right-hand side denotes the coercion from NNReal to $\mathbb{R}$. This is a technical coordinatewise estimate that can be reused whenever a weak Hessian is defined through the derivative of a Lipschitz gradient.

Formalization Note The statement applies in finite-dimensional Euclidean space for every natural number $n$, including $n=0$, and does not assert classical $C^2$ regularity or differentiability everywhere. The Hessian coordinates are expressed using the Lean definition hessianMatrix.

Original Lean declaration header

Within namespace FunctionalInequalities.Probability.Stein. Shown in its original module context. Proof omitted.

theorem norm_hessianMatrix_entry_le_of_lipschitz_gradient {n : ℕ}
    {u : EuclideanSpace ℝ (Fin n) → ℝ} {G : NNReal}
    (hG : LipschitzWith G (gradient u))
    (x : EuclideanSpace ℝ (Fin n)) (i j : Fin n) :
    ‖hessianMatrix u x i j‖ ≤ (G : ℝ)

Module navigation

Module: Analysis/BakryEmery/WeakHessian.

Definition modules: Analysis/BakryEmery/HessianOperator.

Previous: ae_weak_third_derivative_symm · Next: memLp_cutoff_mul_hessianMatrix_entry.

Source excerpt, lines 402–406 · Frozen source 408915f.