Commit 2022-01-15 21:32 1a29adc4

feat(measure_theory/integral): weaker assumptions on Ioi integrability (#11090) To show a function is integrable given an ae_cover it suffices to show boundedness along a filter, not necessarily convergence. This PR adds these generalisations, and uses them to show the older convergence versions.