Integrated Bochner Identity at Lipschitz Regularity

This formalizes the integrated Bochner identity for a $C^{1,1}$ potential; it is related to Lemma A.6 of Letwin (2026), cited as “Brascamp–Lieb for $\nu$.”

Let $E$ be a complete finite-dimensional real inner-product space with its Borel structure. Let $U:E\to\mathbb R$ be $C^1$, let $\nabla U$ be Lipschitz with constant $G\in[0,\infty)$, and let $U$ itself be Lipschitz with constant $L\in[0,\infty)$. Assume

1. $e^{-U}$ is integrable with respect to volume measure.
2. $f:E\to\mathbb R$ is $C^\infty$.
3. $f$ has compact support.

With $\nu=\operatorname{volume}.\operatorname{tilted}(-U)$,

where $\mathcal L_U f=\Delta f-\langle\nabla U,\nabla f\rangle$. The derivative $D(\nabla U)$ is the a.e. derivative fderiv ℝ (gradient U), and the Hessian square is hessianSqStdBasis.

Original Lean declaration header

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

theorem integral_weightedLaplacian_sq_eq_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) :
    ∫ x, weightedLaplacian U f x ^ 2 ∂((volume : Measure E).tilted (-U)) =
      ∫ x, (hessianSqStdBasis f x + ⟪fderiv ℝ (gradient U) x (gradient f x), gradient f x⟫)
        ∂((volume : Measure E).tilted (-U))

Module navigation

Module: Analysis/BakryEmery/Bochner/Lipschitz.

Definition modules: Analysis/BakryEmery/Bochner/Basic, Analysis/BakryEmery/Laplacian.

Supporting theorems: gammaTwo_eq_hessianSqStdBasis_add, exists_contDiff_approx_of_lipschitz_gradient.

Next: compact_ordinary_diffusion_coercivity_of_lipschitz_gradient.

Source excerpt, lines 131–137 · Frozen source 408915f.