memLp_exp_mul — Mathlib

English

If h : HasSubgaussianMGF X c μ, then for all t ∈ ℝ and p ≥ 0, exp(t X) ∈ L^p(μ).

Русский

Если h: HasSubgaussianMGF X c μ, то для всех t ∈ ℝ и p ≥ 0, exp(t X) ∈ L^p(μ).

LaTeX

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

Lean4

theorem memLp_exp_mul (h : HasSubgaussianMGF X c μ) (t : ℝ) (p : ℝ≥0) : MemLp (fun ω ↦ exp (t * X ω)) p μ :=
  by
  rw [HasSubgaussianMGF_iff_kernel] at h
  simpa using h.memLp_exp_mul t p

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