Commit 2026-03-06 15:35 808d25ca

View on Github →

feat(MeasureTheory/Probability): Add more condLExp API (#36271)

Estimated changes

Modified Mathlib/MeasureTheory/Function/ConditionalLExpectation.lean

added theorem MeasureTheory.condLExp_finset_sum

added theorem MeasureTheory.condLExp_one

added theorem MeasureTheory.condLExp_tsum

added theorem MeasureTheory.condLExp_zero