English
For z in the vertical strip where the integrable exponential set condition holds, the nth iterated derivative of the complexMGF at z has a derivative (with respect to z) given by the integral of X^(n+1) times exp(zX) with respect to μ.
Русский
Для z в вертикальной полосе, где выполняется условие интегрируемого экспоненциального множителя, производная n-й итерации комплексной MGФ равна интегралу X^(n+1) e^{zX} по μ.
LaTeX
$$$\\text{HasDerivAt}(\\text{iteratedDeriv}_n(\\text{complexMGF}(X,\\mu)), \\mu[\\omega \\mapsto X(\\omega)^{n+1} \\cdot \\mathrm{cexp}(z X(\\omega))], z)$$$
Lean4
theorem hasDerivAt_iteratedDeriv_complexMGF (hz : z.re ∈ interior (integrableExpSet X μ)) (n : ℕ) :
HasDerivAt (iteratedDeriv n (complexMGF X μ)) μ[fun ω ↦ X ω ^ (n + 1) * cexp (z * X ω)] z := by
induction n generalizing z with
| zero => simp [hasDerivAt_complexMGF hz]
| succ n hn =>
rw [iteratedDeriv_succ]
have : deriv (iteratedDeriv n (complexMGF X μ)) =ᶠ[𝓝 z] fun z ↦ μ[fun ω ↦ X ω ^ (n + 1) * cexp (z * X ω)] :=
by
have h_mem : ∀ᶠ y in 𝓝 z, y.re ∈ interior (integrableExpSet X μ) :=
by
refine IsOpen.eventually_mem ?_ hz
exact isOpen_interior.preimage Complex.continuous_re
filter_upwards [h_mem] with y hy using HasDerivAt.deriv (hn hy)
rw [EventuallyEq.hasDerivAt_iff this]
exact hasDerivAt_integral_pow_mul_exp hz (n + 1)
