Conditional variance

Assume AC. For real $X\in L^2(P)$ define $\mathrm{Var}(X\mid \mathcal{G})=E[(X-E[X\mid \mathcal{G}]{)}^2\mid \mathcal{G}]$ as an almost-sure class. Its integrability, nonnegativity, representative independence and second-moment formula are justified by the following lemma.

The conditional class is Conditional expectation as an ae class, with The Axiom of Choice inherited from existence. By Conditional lp contraction, a version of the conditional mean is square integrable. The unbounded-factor rule Taking out what is known will apply to products whose integrability is verified in the well-definedness lemma, recorded under justified_by.

Durrett §4.1.2, printed pp.211–213, supplies the conditional $L^2$ machinery; the following local lemma establishes the variance formula.