Commit 2022-11-17 16:08 0d4bacdc

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(π).)