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, and lintegral_bind_le.

Estimated changes