analyticOnNhd_mgf

Mathlib.Probability.Moments.MGFAnalytic

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

English

The derivative of mgf at t is ∫ X e^{t X} dμ, for t in the interior region.

Русский

Производная mgf по t равна ∫ X e^{t X} dμ при t внутри области.

LaTeX

$$$\text{HasDerivAt}(\mathrm{mgf}(X, \mu), \int_{\Omega} X(\omega) e^{t X(\omega)} d\mu(\omega), t).$$$

Lean4

theorem analyticOnNhd_mgf : AnalyticOnNhd ℝ (mgf X μ) (interior (integrableExpSet X μ)) := fun _ hx ↦ analyticAt_mgf hx

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

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

Разделы

Аффилиация

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