Integrability of the Weighted Laplacian of Γ

This is a compact-support integrability lemma for the weighted Laplacian applied to a carré-du-champ function.

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. Then

Here weightedLaplacian is $\mathcal L$ and gamma f f is $\Gamma(f,f)=\|\nabla f\|^2$. The statement provides the integrability needed in compactly supported Bochner calculations.

Original Lean declaration header

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

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

Module navigation

Module: Analysis/BakryEmery/Curvature.

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

Previous: convexOn_of_hessian_ge · Next: integrable_gamma_weightedLaplacian.

Source excerpt, lines 114–117 · Frozen source 408915f.