measure_univ_le_one — Mathlib

English

For HasSubgaussianMGF, almost surely the image measure κ ω' is finite.

Русский

Для HasSubgaussianMGF почти наверняка κ ω' — конечная мера.

LaTeX

$$$\\forall^{\\!}\\omega'\\, \\mathrm{IsFiniteMeasure}(\\kappa(\\omega')).$$$

Lean4

theorem measure_univ_le_one (h : HasSubgaussianMGF X c κ ν) : ∀ᵐ ω' ∂ν, κ ω' Set.univ ≤ 1 :=
  by
  filter_upwards [h.isFiniteMeasure, h.mgf_le] with ω' h h_mgf
  suffices (κ ω').real Set.univ ≤ 1 by
    rwa [← ENNReal.ofReal_one, ENNReal.le_ofReal_iff_toReal_le (measure_ne_top _ _) zero_le_one]
  simpa [mgf] using h_mgf 0

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