Prove2Me

Laplacian of the Squared Gradient Norm

Proved
FunctionalInequalities.Analysis.BakryEmery.laplacian_norm_gradient_sq_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is the pointwise expansion of the Laplacian of the squared gradient norm.

Let EE be a complete finite-dimensional real inner-product space, let f:E→Rf:E\to\mathbb R be C3C^3, and let x∈Ex\in E. For the fixed standard orthonormal basis (ei)(e_i),

Δ∥∇f∥2(x)=2∑i∑j(D2f(x)(ei,ej))2+2∑j∂jf(x)∑i∂i∂i∂jf(x).\Delta\|\nabla f\|^2(x) = 2\sum_i\sum_j\bigl(D^2f(x)(e_i,e_j)\bigr)^2 +2\sum_j \partial_jf(x)\sum_i\partial_i\partial_i\partial_jf(x).

The Hessian terms are expressed by bilinearIteratedFDerivTwo; the third-order terms are retained explicitly. The identity is a technical component of the local Bochner identity and includes the dimension-zero case.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis.BakryEmery. Shown in its original module context. Proof omitted.

theorem laplacian_norm_gradient_sq {f : E → ℝ} (hf : ContDiff ℝ 3 f) (x : E) :
    Laplacian.laplacian (fun y => ‖gradient f y‖ ^ 2) x =
      2 * ∑ i, ∑ j,
          (bilinearIteratedFDerivTwo ℝ f x (stdOrthonormalBasis ℝ E i)
            (stdOrthonormalBasis ℝ E j)) ^ 2 +
        2 * ∑ j, fderiv ℝ f x (stdOrthonormalBasis ℝ E j) *
          ∑ i, fderiv ℝ (fun y => fderiv ℝ (fun z => fderiv ℝ f z (stdOrthonormalBasis ℝ E j)) y
            (stdOrthonormalBasis ℝ E i)) x (stdOrthonormalBasis ℝ E i)

Module navigation

Module: Analysis/BakryEmery/Bochner/Basic.

Next: inner_gradient_gradient_laplacian.

Source excerpt, lines 208–215 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Bochner_Basic

universe u
variable {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
variable [CompleteSpace E] [FiniteDimensional ℝ E]
Formal statement

theorem FunctionalInequalities.Analysis.BakryEmery.laplacian_norm_gradient_sq_readable {f : E → ℝ} (hf : ContDiff ℝ 3 f) (x : E) :
    Laplacian.laplacian (fun y => ‖gradient f y‖ ^ 2) x =
      2 * ∑ i, ∑ j,
          (bilinearIteratedFDerivTwo ℝ f x (stdOrthonormalBasis ℝ E i)
            (stdOrthonormalBasis ℝ E j)) ^ 2 +
        2 * ∑ j, fderiv ℝ f x (stdOrthonormalBasis ℝ E j) *
          ∑ i, fderiv ℝ (fun y => fderiv ℝ (fun z => fderiv ℝ f z (stdOrthonormalBasis ℝ E j)) y
            (stdOrthonormalBasis ℝ E i)) x (stdOrthonormalBasis ℝ E i) := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/Bochner/Basic.lean#L207-L242 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.Bochner.Basic`, declaration `FunctionalInequalities.Analysis.BakryEmery.laplacian_norm_gradient_sq`; the repository is private at upload time).

View graph