Theorem MeasureTheory.condExp_stronglyMeasurable_simpleFunc_bilin

Modification history

2025-12-03 18:10
Mathlib/MeasureTheory/Function/ConditionalExpectation/PullOut.lean
feat: generalize the pull-out property of the conditional expectation (#31666) …
Added MeasureTheory.condExp_stronglyMeasurable_simpleFunc_bilinView on Github →