memLp_id_gaussianReal — Mathlib

English

All moments of a real Gaussian distribution are finite: id ∈ Lp for all finite p.

Русский

Все моменты реального гауссовского распределения конечны: идентификатор принадлежит Lp для всех конечных p.

LaTeX

$$$\mathrm{MemLp}(\mathrm{id}, p, GaussianReal(\mu,v))$ for all finite p.$$

Lean4

/-- All the moments of a real Gaussian distribution are finite. That is, the identity is in Lp for
all finite `p`. -/
theorem memLp_id_gaussianReal (p : ℝ≥0) : MemLp id p (gaussianReal μ v) :=
  memLp_of_mem_interior_integrableExpSet (by simp) p

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