Theorem MeasureTheory.Memℒp.condExpL2_ae_eq_condExp

Modification history

2025-02-21 20:26
Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
Rename `Mem𝓛p` to `MemLp` (#22164) …
Deleted MeasureTheory.Memℒp.condExpL2_ae_eq_condExpView on Github →
2025-01-23 12:20
Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
chore(CondExp): golf (#20981) …
Modified MeasureTheory.Memℒp.condExpL2_ae_eq_condExpView on Github →
2025-01-22 16:48
Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
feat: `condExpL2` equals `condExp` for L2 functions (#20945)
Added MeasureTheory.Memℒp.condExpL2_ae_eq_condExpView on Github →