analyticOn_complexMGF — Mathlib

English

The complexified moment generating function complexMGF is analytic on the vertical strip where the real part lies in the interior of the set of integrable exponentials.

Русский

Функция комплексного момента mgf аналитична на вертикальном полосе, где вещественная часть принадлежит внутренности множества интегрируемых экспонент.

LaTeX

$$$\text{AnalyticOn}_{\mathbb{C}}(\text{complexMGF}(X, μ), \\{ z \in \mathbb{C} : z_{re} \in \operatorname{int}(\operatorname{integrableExpSet}(X, μ)) \})$$$

Lean4

/-- `complexMGF X μ` is analytic on the vertical strip
  `{z | z.re ∈ interior (integrableExpSet X μ)}`. -/
theorem analyticOn_complexMGF : AnalyticOn ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet X μ)} :=
  analyticOnNhd_complexMGF.analyticOn

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