Commit 2022-04-10 12:36 32cc8689

feat(measure_theory/measure/measure_space): let measure.map work with ae_measurable functions (#13241) Currently, measure.map f μ is zero if f is not measurable. This means that one can not say that two integrable random variables X and Y have the same distribution by requiring measure.map X μ = measure.map Y μ, as X or Y might not be measurable. We adjust the definition of measure.map to also work with almost everywhere measurable functions. This means that many results in the library that were only true for measurable functions become true for ae measurable functions. We generalize some of the existing code to this more general setting.