Tilted Linear Average as a Log-Laplace Derivative Under a Single Exponential Moment

This is the local tilt-average/derivative identity for linear observables.

Let $E$ be a finite-dimensional real inner-product space with Borel structure, let $\mu$ be a finite nonzero measure, and assume that for some $r\in\mathbb R$,

If $z\in E$ satisfies $\|z\|<r$, then for every $v\in E$,

where $\mu_z$ is the exponential tilt, $\Lambda_\mu=\logLaplace(\mu)$, and the derivative is represented by fderiv ℝ (logLaplace μ) z v. Only the single exponential moment at radius $r$ is assumed.

Original Lean declaration header

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

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

Module navigation

Module: Analysis/BakryEmery/Cumulant/Basic.

Definition modules: Analysis/BakryEmery/Tilt/Basic.

Previous: tiltAverage_inner_eq_fderiv_logLaplace · Next: taylorTensor_inner_eq_cumulant.

Source excerpt, lines 178–180 · Frozen source 408915f.