analyticOnNhd_cgf — Mathlib

English

Let X: Ω → ℝ be a real-valued function on a measure space with measure μ. Then the cumulant generating function cgf(X, μ) is analytic on the interior of the set of real numbers {t : exp(t X) is μ-integrable}. In particular cgf is analytic on int(integrableExpSet(X, μ)).

Русский

Пусть X: Ω → ℝ — функция на измеримом пространстве (Ω, μ). Кумулятивная генераторная функция cgf(X, μ) аналитична на внутренности множества {t : ∫ exp(t X) dμ < ∞}. В частности cgf аналитична на int(integrableExpSet(X, μ)).

LaTeX

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

Lean4

theorem analyticOnNhd_cgf : AnalyticOnNhd ℝ (cgf X μ) (interior (integrableExpSet X μ)) := fun _ hx ↦ analyticAt_cgf hx

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