Commit 2021-04-03 03:51 2a9c21cc

feat(measure_theory/interval_integral): improve integral_comp lemmas (#6795) I expand our collection of integral_comp lemmas so that they can handle all interval integrals of the form ∫ x in a..b, f (c * x + d), for any function f : ℝ → E and any real constants c and d such that c ≠ 0. This PR now also removes the ae_measurable assumptions from the preexisting interval_comp lemmas (thank you @sgouezel!).