English
For each n ∈ ℕ, the n-th derivative of mgf is given by the expectation of X^n e^{t X} under μ, i.e. iteratedDeriv n (mgf X μ)(t) = ∫ X(ω)^n e^{t X(ω)} dμ(ω).
Русский
Для каждого n∈ℕ n-я производная mgf равна интегралу X^n e^{t X} по μ, т.е. iteratedDeriv n (mgf X μ)(t) = ∫ X^n e^{t X} dμ.
LaTeX
$$$\operatorname{iteratedDeriv}(n, \mathrm{mgf}(X, \mu))(t) = \int_{\Omega} X(\omega)^{n} e^{t X(\omega)} \, d\mu(\omega).$$$
Lean4
theorem hasDerivAt_iteratedDeriv_mgf (ht : t ∈ interior (integrableExpSet X μ)) (n : ℕ) :
HasDerivAt (iteratedDeriv n (mgf X μ)) μ[fun ω ↦ X ω ^ (n + 1) * exp (t * X ω)] t := by
induction n generalizing t with
| zero => simp [hasDerivAt_mgf ht]
| succ n hn =>
rw [iteratedDeriv_succ]
have : deriv (iteratedDeriv n (mgf X μ)) =ᶠ[𝓝 t] fun t ↦ μ[fun ω ↦ X ω ^ (n + 1) * exp (t * X ω)] :=
by
have h_mem : ∀ᶠ y in 𝓝 t, y ∈ interior (integrableExpSet X μ) := isOpen_interior.eventually_mem ht
filter_upwards [h_mem] with y hy using HasDerivAt.deriv (hn hy)
rw [EventuallyEq.hasDerivAt_iff this]
exact hasDerivAt_integral_pow_mul_exp_real ht (n + 1)
