English
Let X be a real-valued random variable on Ω with μ a measure. If the real part of z lies in the interior of the set where the exponential moment is integrable, then the complex moment generating function is analytic at z.
Русский
Пусть X — случайная величина на Ω, μ — мера. Если действительная часть z принадлежит внутренности множества, где экспонтенциальный момент интегрируем, то комплексная MGF аналитична в точке z.
LaTeX
$$$\\Re(z) \\in \\operatorname{Int}(\\mathrm{integrableExpSet}(X,\\mu)) \\Rightarrow \\text{Analytic}_{\\mathbb{C}}(\\text{complexMGF}(X,\\mu), z)$$$
Lean4
/-- `complexMGF X μ` is analytic at any point `z` with `z.re ∈ interior (integrableExpSet X μ)`. -/
theorem analyticAt_complexMGF (hz : z.re ∈ interior (integrableExpSet X μ)) : AnalyticAt ℂ (complexMGF X μ) z :=
analyticOnNhd_complexMGF z hz
