Ordinary Diffusion Coercivity with Lipschitz Gradient

This is the coercivity consequence of the integrated Bochner identity at Lipschitz regularity; it is related to Lemma A.6 of Letwin (2026).

Let $E$ be a complete finite-dimensional real inner-product space with its Borel structure. Let $U:E\to\mathbb R$ be $C^1$, with $\nabla U$ Lipschitz with constant $G\in[0,\infty)$ and $U$ Lipschitz with constant $L\in[0,\infty)$. Assume $e^{-U}$ is integrable with respect to volume measure. Let $f:E\to\mathbb R$ be smooth and compactly supported, and set $\nu=\operatorname{volume}.\operatorname{tilted}(-U)$. Then:

1. The function $x\mapsto\langle D(\nabla U)(x)\nabla f(x),\nabla f(x)\rangle$ is $\nu$-integrable.
2. The function $x\mapsto(\mathcal L_Uf(x))^2$ is $\nu$-integrable.
3. The Hessian pairing is bounded above by the squared weighted Laplacian:

This supplies an ordinary diffusion coercivity estimate without a pointwise Hessian lower bound.

Original Lean declaration header

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

theorem compact_ordinary_diffusion_coercivity_of_lipschitz_gradient
    {U : E → ℝ} (hU : ContDiff ℝ 1 U) {G : NNReal}
    (hG : LipschitzWith G (gradient U)) {L : NNReal} (hL : LipschitzWith L U)
    (hexp : Integrable (fun x => Real.exp (-U x)) (volume : Measure E))
    {f : E → ℝ} (hf : ContDiff ℝ ∞ f) (hfc : HasCompactSupport f) :
    Integrable (fun x => ⟪fderiv ℝ (gradient U) x (gradient f x), gradient f x⟫)
      ((volume : Measure E).tilted (-U)) ∧
    Integrable (fun x => weightedLaplacian U f x ^ 2)
      ((volume : Measure E).tilted (-U)) ∧
    (∫ x, ⟪fderiv ℝ (gradient U) x (gradient f x), gradient f x⟫
        ∂((volume : Measure E).tilted (-U))) ≤
      ∫ x, weightedLaplacian U f x ^ 2 ∂((volume : Measure E).tilted (-U))

Module navigation

Module: Analysis/BakryEmery/Bochner/Lipschitz.

Definition modules: Analysis/BakryEmery/Laplacian.

Supporting theorems: integral_weightedLaplacian_sq_eq_of_lipschitz_gradient.

Previous: integral_weightedLaplacian_sq_eq_of_lipschitz_gradient.

Source excerpt, lines 289–300 · Frozen source 408915f.