2022-06-24 09:16
src/measure_theory/function/conditional_expectation.lean
feat(measure_theory/function/conditional_expectation): conditional expectation w.r.t. the restriction of a measure to a set (#14751) …
Added measure_theory.condexp_of_ae_strongly_measurable'