deriv_mgf_zero

Mathlib.Probability.Moments.MGFAnalytic

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.deriv_mgf_zero

English

The derivative of mgf at zero equals the first moment, i.e. d/dt mgf(t)|_{t=0} = ∫ X dμ.

Русский

Производная mgf в нуле равна первому моменту: d/dt mgf(t)|_{t=0} = ∫ X dμ.

LaTeX

$$$\dfrac{d}{dt}\mathrm{mgf}(X, \mu)(t)\big|_{t=0} = \int_{\Omega} X(\omega) \, d\mu(\omega).$$$

Lean4

theorem deriv_mgf_zero (h : 0 ∈ interior (integrableExpSet X μ)) : deriv (mgf X μ) 0 = μ[X] := by simp [deriv_mgf h]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru