mathlib

660918bb - feat(measure_theory/function/conditional_expectation): Conditional expectation of an indicator (#14058)

feat(measure_theory/function/conditional_expectation): Conditional expectation of an indicator (#14058) The main lemma is this: ```lean 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.