Commit 2022-05-25 08:59 660918bb

feat(measure_theory/function/conditional_expectation): Conditional expectation of an indicator (#14058) The main lemma is this:

lemma condexp_indicator (hf_int : integrable f μ) (hs : measurable_set[m] s) :
  μ[s.indicator f | m] =ᵐ[μ] s.indicator (μ[f | m])

We also use it to prove that if two sigma algebras are "equal under an event", then the conditional expectations with respect to those two sigma algebras are equal under the same event.