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)
Deleted AEStronglyMeasurable.norm_condExp_le