isFiniteMeasure — Mathlib

English

For HasSubgaussianMGF, almost surely, the total mass κ ω' of the measure is at most 1; in particular if κ ω' is a probability measure, this is equality.

Русский

Для HasSubgaussianMGF почти наверняка масса меры κ ω' не превышает 1; если κ ω' является вероятностной мерой, массы равны 1.

LaTeX

$$$\\forall^{\\!}\\omega'\\, (\\kappa(\\omega')\\text{-mass} (\\Omega) \\le 1).$$$

Lean4

theorem isFiniteMeasure (h : HasSubgaussianMGF X c κ ν) : ∀ᵐ ω' ∂ν, IsFiniteMeasure (κ ω') :=
  by
  filter_upwards [h.ae_integrable_exp_mul 0, h.mgf_le] with ω' h h_mgf
  simpa [integrable_const_iff] using h

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