Commit 2021-06-15 03:22 ba25bb8a

feat(measure_theory): define measure.trim, restriction of a measure to a sub-sigma algebra (#7906) It is common to see a measure μ on a measurable space structure m0 as being also a measure on any m ≤ m0. Since measures in mathlib have to be trimmed to the measurable space, μ itself is not a measure on m. For hm : m ≤ m0, we define the measure μ.trim hm on m. We add lemmas relating a measure and its trimmed version, mostly about integrals of m-measurable functions.