integrable_exp_mul — Mathlib

English

If X has a conditional subgaussian MGF with parameter c, then for every real t, the function ω ↦ exp(t X(ω)) is integrable with respect to μ.

Русский

Если X обладает условной субгауссовой MGФ с параметром c, то для каждого t функция ω ↦ exp(t X(ω)) интегрируема по mю.

LaTeX

$$$\\forall t \\in \\mathbb{R},\\; \\int_Ω e^{t X(ω)} d\\mu(ω) < \\infty.$$$

Lean4

theorem integrable_exp_mul (h : HasCondSubgaussianMGF m hm X c μ) (t : ℝ) : Integrable (fun ω ↦ exp (t * X ω)) μ :=
  condExpKernel_comp_trim (μ := μ) hm ▸ Kernel.HasSubgaussianMGF.integrable_exp_mul h t

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