ae_integrable_exp_mul — Mathlib

English

For a HasSubgaussianMGF X c κ ν, for every real t, exp(t X) is integrable with respect to κ ω' for ν-almost every ω'.

Русский

Для HasSubgaussianMGF X c κ ν, для каждого t вещественного, экспонента e^{t X} интегрируема по κ ω' для ν-почти каждого ω'.

LaTeX

$$$\\forall t\\in\\mathbb{R},\\ \\forall^{\\!}\\omega'\\partial ν,\\ \\mathrm{Integrable}(\\lambda\\omega: e^{t X(\\omega)})(\\kappa(\\omega')).$$$

Lean4

theorem ae_integrable_exp_mul (h : HasSubgaussianMGF X c κ ν) (t : ℝ) :
    ∀ᵐ ω' ∂ν, Integrable (fun y ↦ exp (t * X y)) (κ ω') :=
  Measure.ae_integrable_of_integrable_comp (h.integrable_exp_mul t)

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