mgf_undef

Mathlib.Probability.Moments.Basic

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

English

If exp(t X) is not integrable with respect to μ, then mgf X μ t is defined to be 0.

Русский

Если exp(t X) не интегрируемо по μ, то mgf(X; μ; t) приравнивается к 0.

LaTeX

$$$\text{mgf}(X; μ; t) = 0$ if $\int e^{t X} dμ$ is undefined$$

Lean4

theorem mgf_undef (hX : ¬Integrable (fun ω => exp (t * X ω)) μ) : mgf X μ t = 0 := by simp only [mgf, integral_undef hX]

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

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

Разделы

Аффилиация

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