differentiableAt_iteratedDeriv_mgf

English

In particular, if v = 0 and 0 lies in the interior of integrableExpSet, then cgf is analytic at 0 with value log mgf(0).

Русский

В частности, при v = 0 и 0 принадлежит interior integrableExpSet, cgf аналитичен в 0 и равен log mgf(0).

LaTeX

$$$\text{AnalyticAt}(\mathbb{R}, \mathrm{cgf}(X, \mu), 0) \text{ if } 0 \in \operatorname{int}(\mathrm{integrableExpSet}(X, \mu)).$$$

Lean4

theorem differentiableAt_iteratedDeriv_mgf (hv : v ∈ interior (integrableExpSet X μ)) (n : ℕ) :
    DifferentiableAt ℝ (iteratedDeriv n (mgf X μ)) v :=
  (analyticAt_iteratedDeriv_mgf hv n).differentiableAt

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