mgf_pos_iff — Mathlib

English

For a nonzero finite measure μ, the mgf is positive exactly when the exponential moment is integrable.

Русский

Для ненулевого конечного меры μ положительно mgf эквивалентно интегрируемости экспоненты аргумента.

LaTeX

$$$[hμ] \ 0 < \mathrm{mgf}(X, μ, t) \iff \operatorname{Integrable}(\lambda \omega. e^{t X(\omega)}) μ$$$

Lean4

theorem mgf_pos_iff [hμ : NeZero μ] : 0 < mgf X μ t ↔ Integrable (fun ω ↦ exp (t * X ω)) μ :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ mgf_pos' hμ.out h⟩
  contrapose! h with h
  simp [mgf_undef h]

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