English
If μ ≠ 0 and exp(t X) is integrable, then mgf X μ t > 0.
Русский
Если μ ≠ 0 и exp(t X) интегрируема, тогда mgf X μ t > 0.
LaTeX
$$$\mathrm{mgf}(X; μ; t) > 0$ provided $μ \neq 0$ and $\int e^{t X} dμ > 0$$$
Lean4
theorem mgf_pos' (hμ : μ ≠ 0) (h_int_X : Integrable (fun ω => exp (t * X ω)) μ) : 0 < mgf X μ t :=
by
simp_rw [mgf]
have : ∫ x : Ω, exp (t * X x) ∂μ = ∫ x : Ω in Set.univ, exp (t * X x) ∂μ := by simp only [Measure.restrict_univ]
rw [this, setIntegral_pos_iff_support_of_nonneg_ae _ _]
· have h_eq_univ : (Function.support fun x : Ω => exp (t * X x)) = Set.univ :=
by
ext1 x
simp only [Function.mem_support, Set.mem_univ, iff_true]
exact (exp_pos _).ne'
rw [h_eq_univ, Set.inter_univ _]
refine Ne.bot_lt ?_
simp only [hμ, ENNReal.bot_eq_zero, Ne, Measure.measure_univ_eq_zero, not_false_iff]
· filter_upwards with x
rw [Pi.zero_apply]
exact (exp_pos _).le
· rwa [integrableOn_univ]
