Vanishing Integral of the Weighted Laplacian

This theorem states the generator identity for a function with polynomial growth.

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

1. $V$ is $C^1$.
2. There are $C_V\in\mathbb R$ and $k_V\in\mathbb N$ such that $\|\nabla V(x)\|\le C_V(1+\|x\|)^{k_V}$.
3. Every exponential moment is integrable with respect to $m.\operatorname{tilted}(-V)$.
4. $f$ is $C^2$ and, for some $C\in\mathbb R$ and $k\in\mathbb N$, the functions $f$, $D f$, and $D^2f$ all have norm bounded by $C(1+\|x\|)^k$ pointwise, with the value bound stated using $|f(x)|$.

Then, writing $\mathcal L=\operatorname{weightedLaplacian}(V,\cdot)$,

This is the polynomial-growth version of the weighted generator identity.

Original Lean declaration header

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

theorem integral_weightedLaplacian_eq_zero_of_growth {V f : E → ℝ} (hV : ContDiff ℝ 1 V)
    {CV : ℝ} {kV : ℕ} (hVg : ∀ x, ‖gradient V x‖ ≤ CV * (1 + ‖x‖) ^ kV)
    (hexp : ∀ r : ℝ, Integrable (fun x => Real.exp (r * ‖x‖)) (m.tilted (-V)))
    (hf : ContDiff ℝ 2 f) {C : ℝ} {k : ℕ}
    (hfg : ∀ x, |f x| ≤ C * (1 + ‖x‖) ^ k ∧ ‖iteratedFDeriv ℝ 1 f x‖ ≤ C * (1 + ‖x‖) ^ k ∧
      ‖iteratedFDeriv ℝ 2 f x‖ ≤ C * (1 + ‖x‖) ^ k) :
    ∫ x, weightedLaplacian V f x ∂(m.tilted (-V)) = 0

Module navigation

Module: Analysis/BakryEmery/Tilt/Temperate.

Definition modules: Analysis/BakryEmery/Laplacian.

Selected supporting theorems: abs_laplacian_le, cutoff_eq_one, hasCompactSupport_cutoff, integrable_of_norm_le_pow, laplacian_mul.

Previous: integrable_of_norm_le_pow.

Source excerpt, lines 357–363 · Frozen source 408915f.