analyticOn_cgf — Mathlib

English

The cumulant generating function cgf(X, μ) is analytic on the interior of integrableExpSet(X, μ).

Русский

К cumulant generating function cgf(X, μ) аналитична на внутренности integrableExpSet(X, μ).

LaTeX

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

Lean4

/-- The cumulant-generating function is analytic on the interior of the interval
  `integrableExpSet X μ`. -/
theorem analyticOn_cgf : AnalyticOn ℝ (cgf X μ) (interior (integrableExpSet X μ)) :=
  analyticOnNhd_cgf.analyticOn

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