Integrated Bochner Formula

Let $E$ be finite-dimensional and complete with a real inner product, let $m$ be an additive Haar measure, and let $V,f:E\to\mathbb R$. Assume that $V$ and $f$ have HasTemperateGrowth, and that every exponential moment is integrable for $\mu=m.\operatorname{tilted}(-V)$. Then

In the formalization, hessianSqStdBasis f represents the squared Hessian Hilbert–Schmidt norm in the standard orthonormal basis, while bilinearIteratedFDerivTwo represents the Hessian bilinear form. This is the integrated Bochner identity on the temperate-growth class.

Original Lean declaration header

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

theorem integral_weightedLaplacian_sq_eq_of_hasTemperateGrowth {V f : E → ℝ}
    (hV : V.HasTemperateGrowth)
    (hexp : ∀ r : ℝ, Integrable (fun x => Real.exp (r * ‖x‖)) (m.tilted (-V)))
    (hf : f.HasTemperateGrowth) :
    ∫ x, weightedLaplacian V f x ^ 2 ∂(m.tilted (-V)) =
      ∫ x, hessianSqStdBasis f x ∂(m.tilted (-V)) +
        ∫ x, bilinearIteratedFDerivTwo ℝ V x (gradient f x) (gradient f x) ∂(m.tilted (-V))

Module navigation

Module: Analysis/BakryEmery/Bochner/Temperate.

Definition modules: Analysis/BakryEmery/Bochner/Basic, Analysis/BakryEmery/Laplacian.

Supporting theorems: gammaTwo_eq_hessianSqStdBasis_add, integrable_of_norm_le_pow, integral_gammaTwo_eq_of_hasTemperateGrowth.

Previous: integral_gammaTwo_eq_of_hasTemperateGrowth · Next: integral_hessianSq_add_le_of_hasTemperateGrowth.

Source excerpt, lines 189–195 · Frozen source 408915f.

Literature

This formalizes Equation (16) of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), cited as Equation (16), p. 6.