ae_aestronglyMeasurable — Mathlib

English

For HasSubgaussianMGF, almost surely with respect to ν, for all real t, exp(t X) is integrable with respect to κ ω'.

Русский

Для HasSubgaussianMGF почти наверняка по ν верно: для каждого t ∈ ℝ экспонента exp(t X) интегрируема по κ ω'.

LaTeX

$$$\\forall\\omega'\\,\\nu,\\ \\forall t\\in\\mathbb{R},\\quad \\mathrm{Integrable}(\\exp(t X),\\kappa(\\omega')).$$$

Lean4

theorem ae_aestronglyMeasurable (h : HasSubgaussianMGF X c κ ν) : ∀ᵐ ω' ∂ν, AEStronglyMeasurable X (κ ω') :=
  by
  have h_int := h.ae_integrable_exp_mul 1
  filter_upwards [h_int] with ω h_int
  simpa using (aemeasurable_of_aemeasurable_exp h_int.1.aemeasurable).aestronglyMeasurable

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