condVar_bot — Mathlib

English

If X is AEMeasurable, then the bottom conditional variance equals the unconditional variance almost surely.

Русский

Если X измеримо в ae-случае, то нижняя условная дисперсия равна безусловной почти наверняка.

LaTeX

$$$\\text{Var}[X; \\mu | \\perp] =^a.e_μ \\; \\text{Var}[X; \\mu]$$$

Lean4

theorem condVar_bot [IsProbabilityMeasure μ] (hX : AEMeasurable X μ) : Var[X; μ | ⊥] = fun _ω ↦ Var[X; μ] := by
  simp [condVar_bot', average_eq_integral, variance_eq_integral hX]

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