Commit 2021-11-21 11:11 55b81f8b

feat(measure_theory): measure preserving maps and integrals (#10326) If f is a measure preserving map, then ∫ y, g y ∂ν = ∫ x, g (f x) ∂μ. It was two rewrites with the old API (hf.map_eq, then a lemma about integral over map measure); it's one rw now. Also add versions for special cases when f is a measurable embedding (in this case we don't need to assume measurability of g).