Integrated Gamma-Two Identity

This theorem gives the integrated identity relating $\Gamma_2$ to the squared weighted Laplacian.

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 function $x\mapsto e^{r\|x\|}$ is integrable with respect to $\mu=m.\operatorname{tilted}(-V)$. Then

The definitions gammaTwo and weightedLaplacian are used for $\Gamma_2$ and $\mathcal L_V$. This identity is the integrated generator form underlying the Bochner formula.

Original Lean declaration header

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

theorem integral_gammaTwo_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, gammaTwo V f x ∂(m.tilted (-V)) = ∫ x, weightedLaplacian V f x ^ 2 ∂(m.tilted (-V))

Module navigation

Module: Analysis/BakryEmery/Bochner/Temperate.

Definition modules: Analysis/BakryEmery/Laplacian, Analysis/BakryEmery/Gamma.

Supporting theorems: integrable_of_norm_le_pow, integral_weightedLaplacian_eq_zero_of_growth, integral_weightedLaplacian_mul_eq_neg_of_hasTemperateGrowth.

Next: integral_weightedLaplacian_sq_eq_of_hasTemperateGrowth.

Source excerpt, lines 147–150 · Frozen source 408915f.