Conditional expectation of indicator functions #

This file proves some results about the conditional expectation of an indicator function and as a corollary, also proves several results about the behaviour of the conditional expectation on a restricted measure.

Main result #

The conditional expectation of the indicator of a function over an m-measurable set with respect to the σ-algebra m is a.e. equal to the indicator of the conditional expectation.

If the restriction to an m-measurable set s of a σ-algebra m is equal to the restriction to s of another σ-algebra m₂ (hypothesis hs), then μ[f | m] =ᵐ[μ.restrict s] μ[f | m₂].