Theorem MeasureTheory.toReal_condLExp

Modification history

2026-03-06 15:35
Mathlib/MeasureTheory/Function/ConditionalExpectation/LebesgueBochner.lean
feat: Radon-Nikodym derivative of a map is a conditional expectation (#35089) …
Added MeasureTheory.toReal_condLExpView on Github →