Theorem MeasureTheory.MemLp.essSup_norm_condExp_le_essSup_norm

Modification history

2026-07-02 09:24
Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean
feat: generalize some lemmas by using conditional Jensen (#36888) …
Added MeasureTheory.MemLp.essSup_norm_condExp_le_essSup_normView on Github →