Polynomial Growth Implies Square Integrability

This theorem gives an $L^2$ consequence of one positive exponential moment.

Let $\mu$ be a probability measure on a measurable normed space $E$. Suppose that some $r>0$ satisfies $x\mapsto e^{r\|x\|}\in L^1(\mu)$. Let $g:E\to\mathbb R$ be continuous and assume that, for some $C\in\mathbb R$ and $k\in\mathbb N$,

Then $g\in L^2(\mu)$, expressed in Lean as MemLp g 2 μ. This is a technical integrability criterion used for polynomially bounded observables.

Original Lean declaration header

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

theorem memLp_of_polynomial_bound_of_integrable_exp (μ : Measure E) [IsProbabilityMeasure μ]
    {r : ℝ} (hr : 0 < r) (hexp : Integrable (fun x => Real.exp (r * ‖x‖)) μ)
    {g : E → ℝ} (hg : Continuous g) {C : ℝ} {k : ℕ}
    (hb : ∀ x, ‖g x‖ ≤ C * (1 + ‖x‖) ^ k) : MemLp g 2 μ

Module navigation

Module: Analysis/BakryEmery/Cumulant/Local.

Previous: cumulant_three_eq_integral_of_integrable_exp · Next: sum_sq_cumulant_three_le_of_letwin_of_integrable_exp.

Source excerpt, lines 186–189 · Frozen source 408915f.