variance_congr

Mathlib.Probability.Moments.Variance

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

English

If X =ᵐ[μ] Y, then Var[X; μ] = Var[Y; μ].

Русский

Если X эквивалентен Y почти surely, дисперсия совпадает.

LaTeX

$$Var[X; μ] = Var[Y; μ] if X =ᵐ[μ] Y$$

Lean4

theorem variance_congr (h : X =ᵐ[μ] Y) : Var[X; μ] = Var[Y; μ] := by simp_rw [variance, evariance_congr h]

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

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

Разделы

Аффилиация

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