complexMGF_undef — Mathlib

English

If X is a-e measurable but rexp(z.re · X) is not integrable, then complexMGF(X, μ, z) = 0.

Русский

Если X измеримо почти всюду, но rexp(z.re · X) не интегрируемо, то complexMGF(X, μ, z) равно 0.

LaTeX

$$$\mathrm{complexMGF}(X, μ, z) = 0 \quad\text{when } \mathrm{AEMeasurable}(X, μ) \wedge \neg\mathrm{Integrable}(\omega \mapsto \mathrm{rexp}(z_{\mathrm{re}} \cdot X(\omega)), μ).$$$

Lean4

theorem complexMGF_undef (hX : AEMeasurable X μ) (h : ¬Integrable (fun ω ↦ rexp (z.re * X ω)) μ) :
    complexMGF X μ z = 0 := by
  rw [complexMGF, integral_undef]
  rw [← integrable_norm_iff (by fun_prop)]
  simpa [Complex.norm_exp] using h

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