English
The expectation of the conditional variance plus the variance of the conditional mean equals the variance of X.
Русский
Ожидание условной дисперсии плюс дисперсия условного математического ожидания равно дисперсии X.
LaTeX
$$$\\mu[\\Var[X; \\mu | m]] + \\Var[\\mu[X|m]; \\mu] = \\Var[X; \\mu]$$$
Lean4
/-- **Law of total variance** -/
theorem integral_condVar_add_variance_condExp (hm : m ≤ m₀) [IsProbabilityMeasure μ] (hX : MemLp X 2 μ) :
μ[Var[X; μ | m]] + Var[μ[X|m]; μ] = Var[X; μ] := by
calc
μ[Var[X; μ | m]] + Var[μ[X|m]; μ]
_ = μ[(μ[X ^ 2|m] - μ[X|m] ^ 2 : Ω → ℝ)] + (μ[μ[X|m] ^ 2] - μ[μ[X|m]] ^ 2) :=
by
congr 1
· exact integral_congr_ae <| condVar_ae_eq_condExp_sq_sub_sq_condExp hm hX
· exact variance_eq_sub hX.condExp
_ = μ[X ^ 2] - μ[μ[X|m] ^ 2] + (μ[μ[X|m] ^ 2] - μ[X] ^ 2) :=
by
rw [integral_sub' integrable_condExp, integral_condExp hm, integral_condExp hm]
exact hX.condExp.integrable_sq
_ = Var[X; μ] := by rw [variance_eq_sub hX]; ring
