iteratedDeriv_mgf_zero — Mathlib

English

The n-th derivative of mgf is equal to the integral of X^n e^{t X} with respect to μ at t, i.e. mgf^{(n)}(t) = ∫ X^n e^{t X} dμ.

Русский

n-я производная mgf равна интегралу X^n e^{t X} по μ: mgf^{(n)}(t) = ∫ X^n e^{t X} dμ.

LaTeX

$$$\operatorname{iteratedDeriv}(n, \mathrm{mgf}(X, \mu))(t) = \int_{\Omega} X(\omega)^{n} e^{t X(\omega)} \, d\mu(\omega).$$$

Lean4

/-- The derivatives of the moment-generating function at zero are the moments. -/
theorem iteratedDeriv_mgf_zero (h : 0 ∈ interior (integrableExpSet X μ)) (n : ℕ) :
    iteratedDeriv n (mgf X μ) 0 = μ[X ^ n] := by simp [iteratedDeriv_mgf h n]

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