variance_eq

Mathlib.Probability.HasLaw

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.HasLaw.variance_eq

← MathLib Explorer

English

If X has law with respect to μ and P, then Var[X; P] = Var[id; μ].

Русский

Если X имеет закон по отношению к μ и P, то Var[X; P] = Var[id; μ].

LaTeX

$$$$ \\operatorname{Var}[X; P] = \\operatorname{Var}[\\mathrm{id}; \\mu] $$$$

Lean4

theorem variance_eq {μ : Measure ℝ} {X : Ω → ℝ} (hX : HasLaw X μ P) : Var[X; P] = Var[id; μ] := by
  rw [← hX.map_eq, variance_map aemeasurable_id hX.aemeasurable, Function.id_comp]

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

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

Разделы

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

Аффилиация

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