Commit 2022-11-08 01:00 946ab799

View on Github →

feat(measure_theory/integral): lintegral_tsum' (#17309) A version of lintegral_supr_directed and lintegral_tsum assuming only ae_measurable and not measurable.

Estimated changes

Modified src/measure_theory/integral/lebesgue.lean

added theorem measure_theory.lintegral_supr_directed_of_measurable

modified theorem measure_theory.lintegral_tsum

Modified src/measure_theory/integral/vitali_caratheodory.lean

Modified src/measure_theory/measure/giry_monad.lean