Theorem MeasureTheory.eLpNorm_condExp_le

Modification history

2026-01-26 14:38
Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
style: consistently put whitespace around pipes in conditional expectation and variance (#33815) …
Modified MeasureTheory.eLpNorm_condExp_leView on Github →
2025-07-09 14:52
Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
chore: fix whitespaces (#26930) …
Modified MeasureTheory.eLpNorm_condExp_leView on Github →
2025-01-23 12:20
Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
chore(CondExp): golf (#20981) …
Modified MeasureTheory.eLpNorm_condExp_leView on Github →
2025-01-22 16:48
Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
feat: `condExpL2` equals `condExp` for L2 functions (#20945)
Added MeasureTheory.eLpNorm_condExp_leView on Github →