mathlib3

1a29adc4 - feat(measure_theory/integral): weaker assumptions on Ioi integrability (#11090)

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.