Coordinate-Norm Bound for Taylor Tensors

This is a coordinate-norm continuity estimate for Taylor tensors.

Let $E$ be a finite-dimensional real inner-product space, let $\mu$ be a probability measure on $E$, and assume that $e^{r\|x\|}$ is $\mu$-integrable for every $r\in\mathbb R$. For an integer $n$, an orthonormal basis $b$ indexed by $\operatorname{Fin}(n)$, and an order $d\in\mathbb N$, there exists $C\in\mathbb R$ such that every $f:E\to\mathbb R$ with $f\in L^2(\mu)$ satisfies

The definition coordTensor uses the chosen basis and taylorTensor denotes $T_d f$. This statement transfers the fixed-order $L^2$ bound to the Hilbert–Schmidt norm of the coefficient array.

Original Lean declaration header

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

theorem exists_norm_coordTensor_taylorTensor_le (μ : Measure E) [IsProbabilityMeasure μ]
    (hexp : ∀ r : ℝ, Integrable (fun x => Real.exp (r * ‖x‖)) μ) {n : ℕ}
    (b : OrthonormalBasis (Fin n) ℝ E) (d : ℕ) :
    ∃ C : ℝ, ∀ f : E → ℝ, MemLp f 2 μ →
      ‖coordTensor b (taylorTensor μ f d)‖ ≤ C * (eLpNorm f 2 μ).toReal

Module navigation

Module: Analysis/BakryEmery/Tilt/SquareIntegrable.

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

Supporting theorems: exists_norm_taylorTensor_le, norm_coordTensor_le.

Previous: exists_norm_taylorTensor_le · Next: integrable_expTilt_of_memLp.

Source excerpt, lines 559–563 · Frozen source 408915f.