mathlib

f21a7605 - feat(measure_theory/function/jacobian): change of variable formula in integrals in higher dimension (#12492)

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