Theorem MeasureTheory.condExp_smul_of_aestronglyMeasurable_right

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