Theorem MeasureTheory.condExp_aestronglyMeasurable_bilin_of_bound

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_aestronglyMeasurable_bilin_of_boundView on Github →