Componentwise Taylor-Field Bound

This statement is the componentwise extension of the Taylor bound to tensor fields.

Let $V$ be a finite-dimensional real inner-product space, let $\nu$ be a probability measure on $V$, and let $R\in\mathbb R$ and $d\in\mathbb N$. Assume that for every scalar $g\in L^2(\nu)$,

where the tensor norm is the Hilbert–Schmidt norm in the standard orthonormal basis. For any rank-$k$ tensor field $u$ represented by Field ν k, the corresponding taylorField satisfies

The result packages a scalar Taylor estimate into the squared norm estimate needed for sums over tensor components. It is reusable whenever a tensor field is handled componentwise.

Formalization Note. normSq is the squared Euclidean norm of the field, and all norms in the conclusion are ordinary real norms.

Original Lean declaration header

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

theorem norm_taylorField_sq_le {R : ℝ} {d : ℕ}
    (h29 : ∀ g : Lp ℝ 2 (ν : Measure V),
      ‖coordTensor (stdOrthonormalBasis ℝ V) (taylorTensor (ν : Measure V) (⇑g) d)‖ ≤
        R ^ d * ‖g‖) {k : ℕ} (u : Field ν k) :
    ‖taylorField d u‖ ^ 2 ≤ R ^ (2 * d) * normSq u

Module navigation

Module: KLS/BKL/PoissonIterate/Criterion.

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

Previous: le_of_iterate_bounds · Next: taylorCriterion.

Source excerpt, lines 346–350 · Frozen source 408915f.