Compactly Supported Gamma-Generator Identity

This is the compactly supported integration-by-parts identity for $\Gamma(f,\mathcal Lf)$.

Let $E$ be finite-dimensional and complete with a real inner product, let $m$ be an additive Haar measure, and let $U,f:E\to\mathbb R$. Assume that $U$ is $C^2$, $f$ is $C^3$, and $f$ has compact support. For $\mu=m.\operatorname{tilted}(-U)$,

Here gamma is the gradient pairing and weightedLaplacian is $\mathcal L_U$. The result is a compact-support component of the curvature and Bochner calculations.

Original Lean declaration header

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

theorem integral_gamma_weightedLaplacian_eq {U f : E → ℝ} (hU : ContDiff ℝ 2 U)
    (hf : ContDiff ℝ 3 f) (hfc : HasCompactSupport f) :
    ∫ x, gamma f (weightedLaplacian U f) x ∂(m.tilted (-U)) =
      -∫ x, weightedLaplacian U f x ^ 2 ∂(m.tilted (-U))

Module navigation

Module: Analysis/BakryEmery/Curvature.

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

Previous: integrable_gamma_weightedLaplacian · Next: mul_integral_gamma_le.

Source excerpt, lines 168–171 · Frozen source 408915f.