Theorem MeasureTheory.condExp_ae_eq_condExpL1CLM
Modification history
2026-05-26 07:57
Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
chore: drop completeness from the definition of conditional expectation (#39862) …
Modified MeasureTheory.condExp_ae_eq_condExpL1CLMView on Github →