Theorem MeasureTheory.condExp_smul_of_aestronglyMeasurable_left

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