integrableExpSet_fun_id_gaussianReal

English

The same as above: the set of t with finite exponential moment for X ∼ Gaussian(μ,v) is all of ℝ.

Русский

То же самое: множество t для которого экспоненциальный момент конечен при X ∼ Gaussian(μ,v) равно всей ℝ.

LaTeX

$$$\mathrm{integrableExpSet}(\mathrm{id}, \mathcal{N}_{\mu,v}) = \mathbb{R}.$$$

Lean4

@[simp]
theorem integrableExpSet_fun_id_gaussianReal : integrableExpSet (fun x ↦ x) (gaussianReal μ v) = Set.univ :=
  integrableExpSet_id_gaussianReal

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