condVar_neg — Mathlib

English

Negating X leaves the conditional variance unchanged almost surely.

Русский

Отрицание X не меняет условную дисперсию почти наверняка.

LaTeX

$$$\\mathrm{Var}[-X; \\mu | m] =^a.e_\\mu \\; \\mathrm{Var}[X; \\mu | m]$$$

Lean4

@[simp]
theorem condVar_neg (X : Ω → ℝ) : Var[-X; μ | m] =ᵐ[μ] Var[X; μ | m] :=
  by
  refine condExp_congr_ae ?_
  filter_upwards [condExp_neg (m := m) X] with ω hω
  simp [hω]
  ring

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