continuousOn_mgf — Mathlib

English

For every n, mgf and all iterated derivatives are analytic on the interior set.

Русский

Для каждого n mgf и все его итеративные производные аналитичны внутри interior.

LaTeX

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

Lean4

theorem continuousOn_mgf : ContinuousOn (mgf X μ) (interior (integrableExpSet X μ)) :=
  differentiableOn_mgf.continuousOn

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