Laplacian Bound by the Hessian Norm

This is a pointwise finite-dimensional estimate for the scalar Laplacian.

Let $E$ be a finite-dimensional real inner-product space, let $g:E\to\mathbb R$ be any function, and let $x\in E$. No differentiability or completeness hypothesis on $g$ is assumed.

Here $D^2g(x)$ is represented by iteratedFDeriv ℝ 2 g x, and $\dim(E)$ is the real vector-space dimension. The estimate is obtained using the fixed standard orthonormal basis and is valid also in dimension zero.

Formalization Note The norm and inequality are real-valued; no measure-theoretic assumptions occur.

Original Lean declaration header

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

theorem abs_laplacian_le (g : E → ℝ) (x : E) :
    |Laplacian.laplacian g x| ≤ Module.finrank ℝ E * ‖iteratedFDeriv ℝ 2 g x‖

Module navigation

Module: Analysis/BakryEmery/Tilt/Temperate.

Previous: norm_iteratedFDeriv_cutoff_le · Next: integrable_of_norm_le_pow.

Source excerpt, lines 179–180 · Frozen source 408915f.