Integrability of Γ Against the Weighted Laplacian

This is a compact-support integrability lemma for the weighted diffusion operator.

Let $m$ be a measure on a finite-dimensional real inner-product space, let $U$ be $C^2$, and let $f$ be $C^3$ with compact support. For the tilted measure $m.\operatorname{tilted}(-U)$, the function $x\mapsto\Gamma(f,\mathcal Lf)(x)$ is integrable:

Here gamma denotes $\Gamma(f,g)=\langle\nabla f,\nabla g\rangle$ and weightedLaplacian denotes $\mathcal L$. The result supplies an integrability side condition for the compactly supported curvature identities.

Original Lean declaration header

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

theorem integrable_gamma_weightedLaplacian {U f : E → ℝ} (hU : ContDiff ℝ 2 U)
    (hf : ContDiff ℝ 3 f) (hfc : HasCompactSupport f) :
    MeasureTheory.Integrable (fun x => gamma f (weightedLaplacian U f) x) (m.tilted (-U))

Module navigation

Module: Analysis/BakryEmery/Curvature.

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

Previous: integrable_weightedLaplacian_gamma · Next: integral_gamma_weightedLaplacian_eq.

Source excerpt, lines 135–137 · Frozen source 408915f.