Commit 2025-04-06 07:30 23f8e103
View on Github →feat(MeasureTheory): add lintegral_bind_le
etc (#23716)
- Drop a measurability assumption in
lintegral_map_le
. - Add
le_join_apply
,lintegral_join_le
,bind_apply_le
, andlintegral_bind_le
.
feat(MeasureTheory): add lintegral_bind_le
etc (#23716)
lintegral_map_le
.le_join_apply
, lintegral_join_le
, bind_apply_le
, and lintegral_bind_le
.