Theorem MeasureTheory.condLExp_ne_top

Modification history

2026-04-13 12:57
Mathlib/MeasureTheory/Function/ConditionalLExpectation.lean
style: fix whitespace (#37993) …
Modified MeasureTheory.condLExp_ne_topView on Github →
2026-03-06 15:35
Mathlib/MeasureTheory/Function/ConditionalLExpectation.lean
feat: Radon-Nikodym derivative of a map is a conditional expectation (#35089) …
Added MeasureTheory.condLExp_ne_topView on Github →