analyticOnNhd_complexMGF — Mathlib

English

The function complexMGF X μ is differentiable on the vertical strip {z : Re z ∈ interior (integrableExpSet X μ)}.

Русский

Функция complexMGF X μ дифференцируема на вертикальной полосе {z : Re z ∈ interior (integrableExpSet X μ)}.

LaTeX

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

Lean4

theorem analyticOnNhd_complexMGF : AnalyticOnNhd ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet X μ)} :=
  differentiableOn_complexMGF.analyticOnNhd (isOpen_interior.preimage Complex.continuous_re)

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