Taylor Tensor Bound for Isotropic Regular Laws

Let $d\in\mathbb N$ satisfy $2\le d$, let $b\in\mathbb R$ satisfy $0<b$, and assume CumulantBound d b. Let $n\in\mathbb N$, let $V:\operatorname{EuclideanSpace}(\mathbb R,\operatorname{Fin} n)\to\mathbb R$, and let $a,b'\in\mathbb R$ be such that hV : KLS.RegularPotential V a b'. Assume that the probability law $\mu=\operatorname{law}(hV)$ is isotropic. For every function $f:\operatorname{EuclideanSpace}(\mathbb R,\operatorname{Fin} n)\to\mathbb R$ with $f\in L^2(\mu)$, the coordinate tensor of the $d$-th Taylor tensor satisfies

where $e$ is the standard basis of $\operatorname{EuclideanSpace}(\mathbb R,\operatorname{Fin} n)$.

This is the assembled Taylor-coefficient estimate for arbitrary square-integrable functions under the stated cumulant bound. It can be reused as the degree-$d\ge2$ input in the Poincaré reduction.

Formalization Note: The tensor norm and the $L^2$ norm are represented by real-valued expressions; eLpNorm takes values in $[0,\infty]$ and is converted with toReal. The statement is finite-dimensional and allows every $n\in\mathbb N$.

Original Lean declaration header

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

theorem norm_coordTensor_taylorTensor_sq_le_two_mul {d : ℕ} (hd : 2 ≤ d) {b : ℝ} (hb : 0 < b)
    (hcb : CumulantBound d b) {n : ℕ} (V : EuclideanSpace ℝ (Fin n) → ℝ) {a b' : ℝ}
    (hV : KLS.RegularPotential V a b') (hiso : KLS.Isotropic hV.law)
    (f : EuclideanSpace ℝ (Fin n) → ℝ) (hf : MemLp f 2 (hV.law : Measure _)) :
    ‖coordTensor (EuclideanSpace.basisFun (Fin n) ℝ) (taylorTensor (hV.law : Measure _) f d)‖ ^ 2 ≤
      2 * b / (d.factorial : ℝ) ^ 2 * (eLpNorm f 2 (hV.law : Measure _)).toReal ^ 2

Module navigation

Module: KLS/BKL/TaylorBound.

Definition modules: KLS/BKL/Suspension/Law, Analysis/Tensor/Coefficients, Analysis/Tensor/Coordinate, KLS/Isotropic, Analysis/BakryEmery/Tilt/Basic, KLS/LogConcave/Regular/Basic.

Selected supporting theorems: convexOn_of_hessian_ge, norm_coordTensor_taylorTensor_inner_sq_le_of_basis, taylorTensor_add, cumulantBound_jointSpace, exists_copies.

Previous: norm_coordTensor_taylorTensor_sq_le_of_smooth.

Source excerpt, lines 503–508 · Frozen source 408915f.

Literature

This formalizes Proposition 7.1 of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), p. 28.