Continuity Bound for Taylor Tensors

This formalizes the operator-norm continuity estimate for Taylor tensors associated with a probability measure having all exponential moments.

Let $E$ be a finite-dimensional real inner-product space, let $\mu$ be a probability measure on $E$, and assume that for every $r\in\mathbb R$ the function $x\mapsto e^{r\|x\|}$ is integrable with respect to $\mu$. Then, for every $d\in\mathbb N$, there exists a real constant $C$ such that every $f:E\to\mathbb R$ with $f\in L^2(\mu)$ satisfies

where taylorTensor μ f d is the Taylor tensor and the Lean expression for the $L^2$ norm is (eLpNorm f 2 μ).toReal.

This gives a boundedness statement for the map $f\mapsto T_d f$ at each fixed order $d$. The constant may depend on $\mu$ and $d$.

Original Lean declaration header

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

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

Module navigation

Module: Analysis/BakryEmery/Tilt/SquareIntegrable.

Definition modules: Analysis/BakryEmery/Tilt/Basic.

Supporting theorems: integrable_exp_mul_norm_of_memLp, iteratedFDeriv_integral_exp_inner_smul.

Previous: taylorTensor_const_mul · Next: exists_norm_coordTensor_taylorTensor_le.

Source excerpt, lines 500–502 · Frozen source 408915f.