First Taylor Tensor Coordinate Formula

This statement identifies each coordinate of the first Taylor tensor for a centered probability measure.

Let $n\in\mathbb N$ and let $\mu$ be a probability measure on $\operatorname{EuclideanSpace}(\mathbb R,\operatorname{Fin} n)$. Assume:

1. For every $r\in\mathbb R$, the function $x\mapsto\exp(r\|x\|)$ is integrable with respect to $\mu$.
2. The identity map belongs to $L^2(\mu)$.
3. The mean of $\mu$ is zero, namely $\int x\,d\mu=0$.
4. The function $f:\operatorname{EuclideanSpace}(\mathbb R,\operatorname{Fin} n)\to\mathbb R$ belongs to $L^2(\mu)$.

Then, for every index map $i:\operatorname{Fin}1\to\operatorname{Fin}n$,

$$\operatorname{coordTensor}(e,\operatorname{taylorTensor}(\mu,f,1))(i) =\int \left\langle e_{i(0)},x\right\rangle f(x)\,d\mu(x),$$

where $e$ is the standard basis.

This is the degree-one coordinate identity used to control the linear Taylor component in the Poincaré reduction.

Formalization Note: The integral and the coordinate tensor are those of coordTensor and taylorTensor; the hypotheses explicitly provide exponential integrability, second-moment integrability, centering, and square integrability.

Original Lean declaration header

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

theorem coordTensor_taylorTensor_one_apply {n : ℕ} (μ : Measure (EuclideanSpace ℝ (Fin n)))
    [IsProbabilityMeasure μ] (hexp : ∀ r : ℝ, Integrable (fun x => Real.exp (r * ‖x‖)) μ)
    (hμ2 : MemLp (id : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) 2 μ)
    (hμ0 : ∫ x, x ∂μ = 0) {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : MemLp f 2 μ)
    (i : Fin 1 → Fin n) :
    coordTensor (EuclideanSpace.basisFun (Fin n) ℝ) (taylorTensor μ f 1) i =
      ∫ x, ⟪EuclideanSpace.basisFun (Fin n) ℝ (i 0), x⟫ * f x ∂μ

Module navigation

Module: KLS/BKL/Reduction.

Definition modules: Analysis/Tensor/Coefficients, Analysis/BakryEmery/Tilt/Basic.

Supporting theorems: taylorTensor_one_apply.

Next: Isotropic.norm_coordTensor_taylorTensor_one_le_of_entries.

Source excerpt, lines 24–30 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Reduction

open MeasureTheory FunctionalInequalities.Analysis.BakryEmery FunctionalInequalities.Analysis.Tensor
open scoped RealInnerProductSpace

theorem FunctionalInequalities.KLS.coordTensor_taylorTensor_one_apply_readable {n : ℕ} (μ : Measure (EuclideanSpace ℝ (Fin n)))
    [IsProbabilityMeasure μ] (hexp : ∀ r : ℝ, Integrable (fun x => Real.exp (r * ‖x‖)) μ)
    (hμ2 : MemLp (id : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) 2 μ)
    (hμ0 : ∫ x, x ∂μ = 0) {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : MemLp f 2 μ)
    (i : Fin 1 → Fin n) :
    coordTensor (EuclideanSpace.basisFun (Fin n) ℝ) (taylorTensor μ f 1) i =
      ∫ x, ⟪EuclideanSpace.basisFun (Fin n) ℝ (i 0), x⟫ * f x ∂μ := by sorry