analyticOn_mgf — Mathlib

English

MGF is analytic on the interior of the set where exponential moments exist.

Русский

MGF аналитичен внутри области существования экспоненциальных моментов.

LaTeX

$$$\operatorname{AnalyticOn}(\mathbb{R}, \mathrm{mgf}(X, \mu), \operatorname{int}(\mathrm{integrableExpSet}(X, \mu))).$$$

Lean4

/-- The moment-generating function is analytic on the interior of the interval on which it is
defined. -/
theorem analyticOn_mgf : AnalyticOn ℝ (mgf X μ) (interior (integrableExpSet X μ)) :=
  analyticOnNhd_mgf.analyticOn

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