Commit 2022-03-16 13:40 f21a7605

feat(measure_theory/function/jacobian): change of variable formula in integrals in higher dimension (#12492) Let μ be a Lebesgue measure on a finite-dimensional real vector space, s a measurable set, and f a function which is differentiable and injective on s. Then ∫ x in f '' s, g x ∂μ = ∫ x in s, |(f' x).det| • g (f x) ∂μ. (There is also a version for the Lebesgue integral, i.e., for ennreal-valued functions).