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]