differentiableOn_mgf — Mathlib

English

The n-th iterated derivative of mgf is analytic on the interior of integrableExpSet.

Русский

n-я итеративная производная mgf аналитична внутри interior integrableExpSet.

LaTeX

$$$\text{AnalyticOnNhd}(\mathbb{R}, \operatorname{iteratedDeriv}(n, \mathrm{mgf}(X, \mu)), \operatorname{int}(\mathrm{integrableExpSet}(X, \mu))).$$$

Lean4

theorem differentiableOn_mgf : DifferentiableOn ℝ (mgf X μ) (interior (integrableExpSet X μ)) := fun _ hx ↦
  (differentiableAt_mgf hx).differentiableWithinAt

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