Extension of Normalized Smooth Taylor Bounds to Affine-Orthogonal $L^2$ Functions

This auxiliary extension statement formalizes a component of Proposition 7.1, p. 28, of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), rather than the full proposition.

Let $d,n\in\mathbb N$, $b\ge0$, and $V:\mathbb R^n\to\mathbb R$. Suppose $h_V:$ RegularPotential $V\ a\ b'$: $a,b'>0$, $V$ is smooth with derivatives of polynomial growth, and $a\operatorname{Id}\le D^2V\le b'\operatorname{Id}$. Let $\mu=h_V.\text{law}$, the normalized $e^{-V}$ law, and assume it is isotropic (KLS.Isotropic). The Euclidean space is EuclideanSpace ℝ (Fin n).

Write $A_d(h)=\operatorname{coord}(T_d^\mu h)$, using taylorTensor and coordTensor in the standard orthonormal basis. Assume that every real-valued $g\in C^2\cap L^2(\mu)$ with a globally bounded second Fréchet derivative, $\int g\,d\mu=0$, $\int g^2\,d\mu=1$, and $\int\langle u,x\rangle g(x)\,d\mu=0$ for all $u$, satisfies $\|A_d(g)\|^2\le b/(d!)^2$.

Then every $f\in L^2(\mu)$ with $\int f\,d\mu=0$ and $\int\langle u,x\rangle f(x)\,d\mu=0$ for all $u$ satisfies

Here the extended norm is eLpNorm, valued in $[0,\infty]$. This is a conditional extension from the stated normalized smooth estimate; no cumulant bound or universal KLS bound is asserted. All natural degrees $d$, including $0$, are allowed.

Original Lean declaration header

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

theorem norm_coordTensor_taylorTensor_sq_le_of_smooth {d : ℕ} {b : ℝ} (hb : 0 ≤ b) {n : ℕ}
    (V : EuclideanSpace ℝ (Fin n) → ℝ) {a b' : ℝ} (hV : KLS.RegularPotential V a b')
    (hiso : KLS.Isotropic hV.law)
    (h113 : ∀ g : EuclideanSpace ℝ (Fin n) → ℝ, ContDiff ℝ 2 g →
      (∃ M : ℝ, ∀ x, ‖fderiv ℝ (fderiv ℝ g) x‖ ≤ M) → MemLp g 2 (hV.law : Measure _) →
      ∫ x, g x ∂(hV.law : Measure _) = 0 →
      ∫ x, g x ^ 2 ∂(hV.law : Measure _) = 1 →
      (∀ u, ∫ x, ⟪u, x⟫ * g x ∂(hV.law : Measure _) = 0) →
      ‖coordTensor (EuclideanSpace.basisFun (Fin n) ℝ) (taylorTensor (hV.law : Measure _) g d)‖ ^ 2 ≤
        b / (d.factorial : ℝ) ^ 2)
    {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : MemLp f 2 (hV.law : Measure _))
    (hf0 : ∫ x, f x ∂(hV.law : Measure _) = 0)
    (hfx : ∀ u, ∫ x, ⟪u, x⟫ * f x ∂(hV.law : Measure _) = 0) :
    ‖coordTensor (EuclideanSpace.basisFun (Fin n) ℝ) (taylorTensor (hV.law : Measure _) f d)‖ ^ 2 ≤
      b / (d.factorial : ℝ) ^ 2 * (eLpNorm f 2 (hV.law : Measure _)).toReal ^ 2

Module navigation

Module: KLS/BKL/TaylorBound.

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

Selected supporting theorems: exists_norm_coordTensor_taylorTensor_le, taylorTensor_add, taylorTensor_const_mul, integrable_exp_mul_norm, contDiff_affineOrthPart.

Next: norm_coordTensor_taylorTensor_sq_le_two_mul.

Source excerpt, lines 387–401 · Frozen source 408915f.