Integrated Curvature Bound for Compactly Supported Tests

This is the integrated $CD(\rho,\infty)$ inequality for a weighted Laplacian.

Let $E$ be a finite-dimensional real inner-product space, let $m$ be an additive Haar measure, and let $U,f:E\to\mathbb R$. Assume:

1. $U$ is $C^2$.
2. $f$ is $C^3$ and has compact support.
3. For some $\rho\in\mathbb R$, every $x,v\in E$ satisfy

With $\mu=m.\operatorname{tilted}(-U)$ and gamma given by $\Gamma(f)=\|\nabla f\|^2$,

This is the integrated coercivity estimate obtained from a pointwise Hessian lower bound and is useful in weighted diffusion arguments.

Original Lean declaration header

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

theorem mul_integral_gamma_le {U f : E → ℝ} (hU : ContDiff ℝ 2 U) (hf : ContDiff ℝ 3 f)
    (hfc : HasCompactSupport f) {ρ : ℝ}
    (hH : ∀ x v, ρ * ‖v‖ ^ 2 ≤ bilinearIteratedFDerivTwo ℝ U x v v) :
    ρ * ∫ x, gamma f 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.

Supporting theorems: gammaTwo_eq_hessianSqStdBasis_add, integrable_gamma_weightedLaplacian, integrable_weightedLaplacian_gamma, integral_gamma_weightedLaplacian_eq.

Previous: integral_gamma_weightedLaplacian_eq.

Source excerpt, lines 211–214 · Frozen source 408915f.