deriv_mgf — Mathlib

English

If the interior condition holds for mgf, then the cumulant generating function cgf, defined as log(mgf), is analytic at v in that interior, provided mgf(X, μ)(v) > 0.

Русский

При натуральном условии аналитичности mgf, логарифм mgf образует cgf, который аналитичен в той же точке, если mgf(X, μ)(v) > 0.

LaTeX

$$$\text{AnalyticAt}_{\mathbb{R}}\bigl(\mathrm{cgf}(X, \mu), v\bigr) \quad \text{при } v \in \operatorname{int}(\mathrm{integrableExpSet}(X, \mu)).$$$

Lean4

/-- For `t ∈ interior (integrableExpSet X μ)`, the derivative of `mgf X μ` at `t` is
`μ[X * exp (t * X)]`. -/
theorem deriv_mgf (h : t ∈ interior (integrableExpSet X μ)) : deriv (mgf X μ) t = μ[fun ω ↦ X ω * exp (t * X ω)] :=
  (hasDerivAt_mgf h).deriv

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