English
For z with Re(z) in the interior of the integrableExpSet, the nth iterated derivative of the complexMGF at z equals the integral of X^n times exp(zX).
Русский
Пусть z удовлетворяет условиям, затем n-я итеративная производная комплексной MGФ в z равна интегралу X^n e^{zX} dμ.
LaTeX
$$$\\operatorname{iteratedDeriv}_n(\\text{complexMGF}(X,\\mu))\\,(z) = \\mu[X^{n} \\cdot \\mathrm{cexp}(zX)]$$$
Lean4
/-- For `z : ℂ` with `z.re ∈ interior (integrableExpSet X μ)`, the n-th derivative of the function
`complexMGF X μ` at `z` is `μ[X ^ n * cexp (z * X)]`. -/
theorem iteratedDeriv_complexMGF (hz : z.re ∈ interior (integrableExpSet X μ)) (n : ℕ) :
iteratedDeriv n (complexMGF X μ) z = μ[fun ω ↦ X ω ^ n * cexp (z * X ω)] := by
induction n generalizing z with
| zero => simp [complexMGF]
| succ n hn =>
rw [iteratedDeriv_succ]
exact (hasDerivAt_iteratedDeriv_complexMGF hz n).deriv
