mathlib

3ee6248c - feat(measure_theory): links between an integral and its improper version (#7164)

feat(measure_theory): links between an integral and its improper version (#7164) This PR introduces ways of studying and computing `∫ x, f x ∂μ` by studying the limit of the sequence `∫ x in φ n, f x ∂μ` for an appropriate sequence `φ` of subsets of the domain of `f`.