Tilted Generator Identity

Let $E$ be a complete finite-dimensional real inner-product space with its Borel measurable structure, and let $m$ be a measure that is an additive Haar measure. Let $V,f:E\to\mathbb R$ satisfy:

1. $V$ is $C^1$.
2. $f$ is $C^2$.
3. $f$ has compact support.

For every $z\in E$, with $\mu=m.\operatorname{tilted}(-V)$, one has

$$F_{-\mathcal Lf}(z)=\left\langle z,F_{\nabla f}(z)\right\rangle,$$

where $F_h=\operatorname{tiltAverage}(\mu,h)$ and

$$\mathcal Lf=\Delta f-\langle\nabla V,\nabla f\rangle.$$

This is the generator identity used to convert weighted-Laplacian terms into gradient terms in the Taylor-tensor argument.

Formalization Note The statement is total even when $e^{-V}$ is not $m$-integrable: in that case the tilted measure is the zero measure and both sides vanish. No probability-measure assumption is present.

Original Lean declaration header

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

theorem tiltAverage_neg_weightedLaplacian {V f : E → ℝ} (hV : ContDiff ℝ 1 V)
    (hf : ContDiff ℝ 2 f) (hfc : HasCompactSupport f) (z : E) :
    tiltAverage (m.tilted (-V)) (fun x => -weightedLaplacian V f x) z =
      ⟪z, tiltAverage (m.tilted (-V)) (gradient f) z⟫

Module navigation

Module: Analysis/BakryEmery/Tilt/Basic.

Definition modules: Analysis/BakryEmery/Laplacian.

Supporting theorems: expTilt_tilted, gradient_sub_inner, integrable_gradient_expTilt, weightedLaplacian_eq_zero_of_notMem_tsupport.

Previous: integrable_gradient_expTilt.

Source excerpt, lines 156–159 · Frozen source 408915f.

Literature

This formalizes Equation (48) of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), Equation (48), p. 14.

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Tilt_Basic

open scoped RealInnerProductSpace ContDiff
universe u
variable {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
variable (m : MeasureTheory.Measure E) [m.IsAddHaarMeasure]

theorem FunctionalInequalities.Analysis.BakryEmery.tiltAverage_neg_weightedLaplacian_readable {V f : E → ℝ} (hV : ContDiff ℝ 1 V)
    (hf : ContDiff ℝ 2 f) (hfc : HasCompactSupport f) (z : E) :
    tiltAverage (m.tilted (-V)) (fun x => -weightedLaplacian V f x) z =
      ⟪z, tiltAverage (m.tilted (-V)) (gradient f) z⟫ := by sorry