First Taylor Coordinate Tensor Bound Given Its Entry Formula

This is a conditional first-order Taylor tensor norm bound under isotropy.

Let $n\in\mathbb N$, $E=$ EuclideanSpace ℝ (Fin n), and $(e_j)$ its standard orthonormal basis. Assume:

1. $\mu$ is an isotropic probability measure (KLS.Isotropic), meaning finite second moment, zero mean, and identity covariance.
2. $f:E\to\mathbb R$ satisfies MemLp f 2 μ.
3. The coordinate array $A=$ Analysis.Tensor.coordTensor of Analysis.BakryEmery.taylorTensor μ f 1 satisfies, for every $i:\operatorname{Fin}(1)\to\operatorname{Fin}(n)$,

$$A_i=\int\langle e_{i(0)},x\rangle f(x)\,d\mu(x).$$

Then its Euclidean coordinate norm satisfies

$$\|A\|\le\bigl(\operatorname{eLpNorm}(f,2,\mu)\bigr).\operatorname{toReal}.$$

This supplies the first-order tensor estimate when the entry identity is available; it does not establish that identity.

Formalization Note eLpNorm takes values in $[0,\infty]$, and the statement explicitly uses its toReal. The MemLp hypothesis ensures finiteness. No log-concavity, smoothness, or positive-dimension assumption is imposed.

Original Lean declaration header

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

theorem Isotropic.norm_coordTensor_taylorTensor_one_le_of_entries {n : ℕ}
    {μ : ProbabilityMeasure (EuclideanSpace ℝ (Fin n))} (hiso : Isotropic μ)
    {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : MemLp f 2 (μ : Measure (EuclideanSpace ℝ (Fin n))))
    (hentry : ∀ i : Fin 1 → Fin n,
      coordTensor (EuclideanSpace.basisFun (Fin n) ℝ)
          (taylorTensor (μ : Measure (EuclideanSpace ℝ (Fin n))) f 1) i =
        ∫ x, ⟪EuclideanSpace.basisFun (Fin n) ℝ (i 0), x⟫ * f x ∂(μ : Measure (EuclideanSpace ℝ (Fin n)))) :
    ‖coordTensor (EuclideanSpace.basisFun (Fin n) ℝ)
        (taylorTensor (μ : Measure (EuclideanSpace ℝ (Fin n))) f 1)‖ ≤
      (eLpNorm f 2 (μ : Measure (EuclideanSpace ℝ (Fin n)))).toReal

Module navigation

Module: KLS/BKL/Reduction.

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

Supporting theorems: integral_sq_eq_affine_decomposition.

Previous: coordTensor_taylorTensor_one_apply · Next: poincare_le_of_cumulantBound.

Source excerpt, lines 49–58 · 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.Isotropic.norm_coordTensor_taylorTensor_one_le_of_entries_readable {n : ℕ}
    {μ : ProbabilityMeasure (EuclideanSpace ℝ (Fin n))} (hiso : Isotropic μ)
    {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : MemLp f 2 (μ : Measure (EuclideanSpace ℝ (Fin n))))
    (hentry : ∀ i : Fin 1 → Fin n,
      coordTensor (EuclideanSpace.basisFun (Fin n) ℝ)
          (taylorTensor (μ : Measure (EuclideanSpace ℝ (Fin n))) f 1) i =
        ∫ x, ⟪EuclideanSpace.basisFun (Fin n) ℝ (i 0), x⟫ * f x ∂(μ : Measure (EuclideanSpace ℝ (Fin n)))) :
    ‖coordTensor (EuclideanSpace.basisFun (Fin n) ℝ)
        (taylorTensor (μ : Measure (EuclideanSpace ℝ (Fin n))) f 1)‖ ≤
      (eLpNorm f 2 (μ : Measure (EuclideanSpace ℝ (Fin n)))).toReal := by sorry