English
For each natural n, the n-th iterated derivative of mgf is analytic on the interior of integrableExpSet(X, μ).
Русский
Для каждого n-го итеративного производного mgf аналитичен на interior integrableExpSet(X, μ).
LaTeX
$$$\operatorname{AnalyticOnNhd}(\mathbb{R}, (\operatorname{iteratedDeriv}(n, \mathrm{mgf}(X, \mu))), \operatorname{int}(\mathrm{integrableExpSet}(X, \mu))).$$$
Lean4
/-- For `t ∈ interior (integrableExpSet X μ)`, the n-th derivative of `mgf X μ` at `t` is
`μ[X ^ n * exp (t * X)]`. -/
theorem iteratedDeriv_mgf (ht : t ∈ interior (integrableExpSet X μ)) (n : ℕ) :
iteratedDeriv n (mgf X μ) t = μ[fun ω ↦ X ω ^ n * exp (t * X ω)] := by
induction n generalizing t with
| zero => simp [mgf]
| succ n hn =>
rw [iteratedDeriv_succ]
exact (hasDerivAt_iteratedDeriv_mgf ht n).deriv
