differentiableAt_mgf — Mathlib

English

The mgf is differentiable at every interior point of integrableExpSet(X, μ).

Русский

MGF дифференцируем в любой точке внутри interior integrableExpSet(X, μ).

LaTeX

$$$\text{DifferentiableAt}(\mathbb{R}, \mathrm{mgf}(X, \mu), t)$ для всех $t \in \operatorname{int}(\mathrm{integrableExpSet}(X, \mu)).$$$

Lean4

theorem differentiableAt_mgf (ht : t ∈ interior (integrableExpSet X μ)) : DifferentiableAt ℝ (mgf X μ) t :=
  (analyticAt_mgf ht).differentiableAt

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