2022-07-16 11:29
src/measure_theory/function/conditional_expectation.lean
feat(measure_theory/function/uniform_integrable): conditional expectations form a uniformly integrable class (#15378) …
Added measure_theory.integrable.uniform_integrable_condexp