differentiableOn_complexMGF — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- `complexMGF X μ` is holomorphic on the vertical strip
`{z | z.re ∈ interior (integrableExpSet X μ)}`. -/
theorem differentiableOn_complexMGF :
    DifferentiableOn ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet X μ)} :=
  by
  intro z hz
  have h := hasDerivAt_complexMGF hz
  rw [hasDerivAt_iff_hasFDerivAt] at h
  exact h.hasFDerivWithinAt.differentiableWithinAt

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