Theorem norm_condExp_le

Modification history

2026-07-02 09:24
Mathlib/MeasureTheory/Function/ConditionalExpectation/CondJensen.lean
feat: generalize some lemmas by using conditional Jensen (#36888) …
Modified norm_condExp_leView on Github →
2026-04-07 09:25
Mathlib/MeasureTheory/Function/ConditionalExpectation/CondJensen.lean
feat: if `f` lies in a closed convex set `s` almost everywhere, then its conditional expectation also lies in `s` almost everywhere (#36638)
Added norm_condExp_leView on Github →