Probabilistic properties of the conditional expectation #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file contains some properties about the conditional expectation which does not belong in
the main conditional expectation file.
Main result #
m₁, m₂ are independent σ-algebras and
𝔼[f | m₂] = 𝔼[f]