variance_of_integral_eq_zero

Mathlib.Probability.Moments.Variance

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

← MathLib Explorer

English

If hX is AE and μ[X] = 0, then variance X μ = ∫ X^2 dμ.

Русский

Если X среднеуправляется AE и μ[X] = 0, то дисперсия X равна ∫ X^2 dμ.

LaTeX

$$variance X μ = ∫ ω X(ω)^2 ∂μ$$

Lean4

theorem variance_of_integral_eq_zero (hX : AEMeasurable X μ) (hXint : μ[X] = 0) : variance X μ = ∫ ω, X ω ^ 2 ∂μ := by
  simp [variance_eq_integral hX, hXint]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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