analyticAt_mgf — Mathlib

English

The mgf is analytic at zero and its Taylor coefficients give the moments μ[X^n].

Русский

MGF аналитичен в нуле, а коэффициенты тейлора дают моменты μ[X^n].

LaTeX

$$$\text{AnalyticAt}(\mathrm{mgf}(X, \mu), 0) = \text{coefficients given by } \frac{\mu[X^n]}{n!}.$$$

Lean4

/-- The moment-generating function is analytic at every `t ∈ interior (integrableExpSet X μ)`. -/
theorem analyticAt_mgf (ht : t ∈ interior (integrableExpSet X μ)) : AnalyticAt ℝ (mgf X μ) t :=
  by
  rw [← re_complexMGF_ofReal']
  exact (analyticAt_complexMGF (by simp [ht])).re_ofReal

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