moment_zero_measure

Mathlib.Probability.Moments.Basic

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

English

For any X and p, moment X p (0) equals 0, i.e., integrating X^p with respect to the zero measure yields zero.

Русский

Для любого X и p момент X p по нулевой мере равен нулю: интегрирование X^p по нулевой мере дает нуль.

LaTeX

$$moment(X,p,0)=0$$

Lean4

@[simp]
theorem moment_zero_measure : moment X p (0 : Measure Ω) = 0 := by simp [moment]

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

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

Разделы

Аффилиация

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