mathlib3

ba25bb8a - feat(measure_theory): define `measure.trim`, restriction of a measure to a sub-sigma algebra (#7906)

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. Co-authored-by: Rémy Degenne <remydegenne@gmail.com>