aestronglyMeasurable — Mathlib

English

If X has a subgaussian MGF, then X is AEStronglyMeasurable with respect to μ.

Русский

Если X обладает субгaуссовой MGФ, то X является AEStronglyMeasurable относительно μ.

LaTeX

$$$\\text{AEStronglyMeasurable}(X, \\mu)$$$

Lean4

theorem aestronglyMeasurable (h : HasSubgaussianMGF X c μ) : AEStronglyMeasurable X μ :=
  by
  have h_int := h.integrable_exp_mul 1
  simpa using (aemeasurable_of_aemeasurable_exp h_int.1.aemeasurable).aestronglyMeasurable

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