Additivity of the Taylor Tensor on $L^2(\mu)$

This is a technical additivity statement for the Taylor tensor taylorTensor associated with tilt averages.

Let $E$ be a finite-dimensional real inner-product normed additive group equipped with its Borel measurable structure, and let $\mu$ be a finite, nonzero measure on $E$. Assume that:

1. For every real number $r$, the function $x \mapsto \exp(r\lVert x\rVert)$ is integrable with respect to $\mu$.
2. The functions $f,g : E \to \mathbb{R}$ belong to $L^2(\mu)$, expressed in Lean as MemLp f 2 μ and MemLp g 2 μ.
3. $d$ is a natural number.

Then the Taylor tensor of the pointwise sum $f+g$ is the sum of the individual Taylor tensors:

This declaration records the linearity of the Taylor-tensor construction on square-integrable functions and can be reused whenever the stated exponential-moment and $L^2$ hypotheses hold.

Formalization Note The measure is only assumed finite and nonzero, not necessarily a probability measure. The equality is asserted for every natural-number order $d$ in the finite-dimensional space $E$; the MemLp hypotheses use exponent $2$ with respect to $\mu$.

Original Lean declaration header

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

theorem taylorTensor_add (μ : Measure E) [IsFiniteMeasure μ] [NeZero μ]
    (hexp : ∀ r : ℝ, Integrable (fun x => Real.exp (r * ‖x‖)) μ) {f g : E → ℝ} (hf : MemLp f 2 μ)
    (hg : MemLp g 2 μ) (d : ℕ) :
    taylorTensor μ (fun x => f x + g x) d = taylorTensor μ f d + taylorTensor μ g d

Module navigation

Module: Analysis/BakryEmery/Tilt/SquareIntegrable.

Definition modules: Analysis/BakryEmery/Tilt/Basic.

Supporting theorems: contDiff_tiltAverage_of_memLp, integrable_exp_mul_norm_of_memLp.

Previous: contDiff_tiltAverage_of_memLp · Next: taylorTensor_const_mul.

Source excerpt, lines 360–363 · Frozen source 408915f.