Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-01-22 16:48
d9e9d6ef
View on Github →
feat:
condExpL2
equals
condExp
for L2 functions (
#20945
)
Estimated changes
Modified
Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
added
theorem
MeasureTheory.Memℒp.condExpL2_ae_eq_condExp'
added
theorem
MeasureTheory.Memℒp.condExpL2_ae_eq_condExp
added
theorem
MeasureTheory.eLpNorm_condExp_le