hasDerivAt_complexMGF — Mathlib

English

The complexMGF is analytic in a neighborhood of the vertical strip {z : Re z ∈ interior (integrableExpSet X μ)}.

Русский

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

LaTeX

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

Lean4

/-- For all `z : ℂ` with `z.re ∈ interior (integrableExpSet X μ)`,
`complexMGF X μ` is differentiable at `z` with derivative `μ[X * exp (z * X)]`. -/
theorem hasDerivAt_complexMGF (hz : z.re ∈ interior (integrableExpSet X μ)) :
    HasDerivAt (complexMGF X μ) μ[fun ω ↦ X ω * cexp (z * X ω)] z :=
  by
  convert hasDerivAt_integral_pow_mul_exp hz 0
  · simp [complexMGF]
  · simp

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