2024-06-22 12:48
Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
feat(MeasureTheory/Function/ConditionalExpectation): relax `integral_condexp` assumption and add `integral_condexp_indicator` (#13932) …
Added MeasureTheory.integral_condexp_indicator