Tilted Linear Average as a Log-Laplace Derivative Under All Exponential Moments

This is the linear-function identity used in the proof of Proposition 7.1 of Bizeul–Klartag–Lehec (arXiv:2610.05474v1).

Let $\mu$ be a finite nonzero measure on a finite-dimensional real inner-product space $E$. Assume that for every $r\in\mathbb R$, $x\mapsto e^{r\|x\|}$ is integrable with respect to $\mu$. Then for all $v,z\in E$,

where $\Lambda_\mu=\operatorname{logLaplace}(\mu)$.

The statement identifies the tilted expectation of a linear observable with the corresponding directional derivative of the logarithmic Laplace transform.

Original Lean declaration header

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

theorem tiltAverage_inner_eq_fderiv_logLaplace (μ : Measure E) [IsFiniteMeasure μ] [NeZero μ]
    (hexp : ∀ r : ℝ, Integrable (fun x => Real.exp (r * ‖x‖)) μ) (v z : E) :
    tiltAverage μ (fun x => ⟪v, x⟫) z = fderiv ℝ (logLaplace μ) z v

Module navigation

Module: Analysis/BakryEmery/Cumulant/Basic.

Definition modules: Analysis/BakryEmery/Tilt/Basic.

Next: tiltAverage_inner_eq_fderiv_logLaplace_of_lt.

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