analyticOn_iteratedDeriv_mgf — Mathlib

English

For any n, the function t ↦ iteratedDeriv n (mgf X μ)(t) is analytic at any interior point v.

Русский

Для любого n функция t ↦ iteratedDeriv n (mgf X μ)(t) аналитична в любой interior точке v.

LaTeX

$$$\text{AnalyticAt}(\mathbb{R}, \operatorname{iteratedDeriv}(n, \mathrm{mgf}(X, \mu)), v).$$$

Lean4

theorem analyticOn_iteratedDeriv_mgf (n : ℕ) :
    AnalyticOn ℝ (iteratedDeriv n (mgf X μ)) (interior (integrableExpSet X μ)) :=
  (analyticOnNhd_iteratedDeriv_mgf n).analyticOn

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