Polynomial Growth Implies Integrability

This theorem gives integrability of a vector-valued function under all exponential moments.

Let $E$ be a measurable normed space, let $F$ be a normed additive group, and let $\mu$ be a measure such that $e^{r\|x\|}$ is integrable for every $r\in\mathbb R$. Suppose that $g:E\to F$ is strongly measurable almost everywhere and that, for some $C\in\mathbb R$ and $k\in\mathbb N$,

Then $g$ is integrable with respect to $\mu$. The result is a general domination lemma for polynomially bounded functions.

Original Lean declaration header

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

theorem integrable_of_norm_le_pow {F : Type*} [NormedAddCommGroup F] (μ : Measure E)
    (hexp : ∀ r : ℝ, Integrable (fun x => Real.exp (r * ‖x‖)) μ) {g : E → F}
    (hg : AEStronglyMeasurable g μ) {C : ℝ} {k : ℕ} (hgb : ∀ x, ‖g x‖ ≤ C * (1 + ‖x‖) ^ k) :
    Integrable g μ

Module navigation

Module: Analysis/BakryEmery/Tilt/Temperate.

Previous: abs_laplacian_le · Next: integral_weightedLaplacian_eq_zero_of_growth.

Source excerpt, lines 226–229 · Frozen source 408915f.