memLp_exp_mul — Mathlib

English

If X has a conditional subgaussian MGF with parameter c, then for every real t and every p ≥ 0, the function ω ↦ exp(t X(ω)) belongs to L^p(μ).

Русский

Если X обладает условной субгауссовой MGФ с параметром c, то для каждого действительного t и каждого p ≥ 0 функция ω ↦ exp(t X(ω)) принадлежит L^p(μ).

LaTeX

$$$\\forall t \\in \\mathbb{R}, \\forall p \\in \\mathbb{R}_{\\ge 0},\\; \\exp(t X) \\in L^p(\\mu).$$$

Lean4

theorem memLp_exp_mul (h : HasCondSubgaussianMGF m hm X c μ) (t : ℝ) (p : ℝ≥0) : MemLp (fun ω ↦ exp (t * X ω)) p μ :=
  condExpKernel_comp_trim (μ := μ) hm ▸ Kernel.HasSubgaussianMGF.memLp_exp_mul h t p

Похожие утверждения