mathlib3

0d4bacdc - feat(measure_theory/integral): substitution without continuity at endpoints (#17540)

feat(measure_theory/integral): substitution without continuity at endpoints (#17540) This PR generalises the substitution law `∫ x in a..b, (g ∘ f) x * f' x = ∫ u in f a..f b, g u` to remove the assumption that `g` be continuous at the endpoints of the interval. (A subsequent PR will use this to prove that `Γ(1/2) = sqrt(π)`.)