ofReal_variance

Mathlib.Probability.Moments.Variance

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

← MathLib Explorer

English

For IsFinite μ and MemLp X 2 μ, .ofReal(variance X μ) = evariance X μ.

Русский

При IsFinite μ и MemLp X 2 μ, .ofReal(variance X μ) = evariance X μ.

LaTeX

$$ .ofReal (variance X μ) = evariance X μ$$

Lean4

theorem ofReal_variance [IsFiniteMeasure μ] (hX : MemLp X 2 μ) : .ofReal (variance X μ) = evariance X μ :=
  by
  rw [variance, ENNReal.ofReal_toReal]
  exact evariance_ne_top hX

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

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

Разделы

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

Аффилиация

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