First Taylor Tensor as a Centered Moment

This formalizes the centered first-moment formula for the first Taylor tensor.

Let $E$ be a finite-dimensional real inner-product space with its Borel measurable structure, and let $\mu$ be a probability measure on $E$. Assume:

1. For every $r\in\mathbb R$, $x\mapsto e^{r\|x\|}$ is integrable with respect to $\mu$.
2. $f:E\to\mathbb R$ belongs to $L^2(\mu)$.
3. $w\in E$.

Writing $T_d f$ for taylorTensor μ f d, the first tensor evaluated at $w$ satisfies

This identifies the first Taylor tensor with the centered first moment and provides the degree-one case used in tensor and cumulant calculations.

Formalization Note The measure is a probability measure, and all displayed integrals are ordinary real-valued integrals under the stated integrability consequences of the hypotheses.

Original Lean declaration header

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

theorem taylorTensor_one_apply (μ : Measure E) [IsProbabilityMeasure μ]
    (hexp : ∀ r : ℝ, Integrable (fun x => Real.exp (r * ‖x‖)) μ) {f : E → ℝ}
    (hf : MemLp f 2 μ) (w : E) :
    taylorTensor μ f 1 (fun _ => w) =
      (∫ x, ⟪w, x⟫ * f x ∂μ) - (∫ x, f x ∂μ) * ∫ x, ⟪w, x⟫ ∂μ

Module navigation

Module: Analysis/BakryEmery/Tilt/LocalDerivatives.

Definition modules: Analysis/BakryEmery/Tilt/Basic.

Supporting theorems: contDiff_tiltAverage_of_memLp, integrable_exp_mul_norm_of_memLp.

Source excerpt, lines 168–172 · Frozen source 408915f.