Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-03 21:49 ec0b1144

View on Github →

feat(measure_theory/group/prod.lean): use measure_preserving predicate (#16668)

Also use quasi_measure_preserving more in various files. In particular, ae_[strongly_]measurable.comp_measurable' is now .comp_quasi_measure_preserving.
Remove lemmas that are direct consequences of [quasi_]measure_preserving properties.
This simplifies various proofs.

Estimated changes

Modified src/analysis/convolution.lean

Modified src/measure_theory/constructions/prod.lean

added theorem measure_theory.measure.measure_preserving_swap

deleted theorem measure_theory.measure.prod_fst_absolutely_continuous

deleted theorem measure_theory.measure.prod_snd_absolutely_continuous

added theorem measure_theory.measure.quasi_measure_preserving_fst

added theorem measure_theory.measure.quasi_measure_preserving_snd

Modified src/measure_theory/function/strongly_measurable.lean

deleted theorem measure_theory.ae_strongly_measurable.comp_measurable'

added theorem measure_theory.ae_strongly_measurable.comp_quasi_measure_preserving

Modified src/measure_theory/group/measure.lean

added theorem measure_theory.measure_preserving_div_right

Modified src/measure_theory/group/prod.lean

deleted theorem measure_theory.map_div_left_absolutely_continuous

deleted theorem measure_theory.map_inv_absolutely_continuous

deleted theorem measure_theory.map_mul_right_absolutely_continuous

deleted theorem measure_theory.map_prod_inv_mul_eq

deleted theorem measure_theory.map_prod_inv_mul_eq_swap

deleted theorem measure_theory.map_prod_mul_eq

deleted theorem measure_theory.map_prod_mul_eq_swap

deleted theorem measure_theory.map_prod_mul_inv_eq

added theorem measure_theory.measure_preserving_mul_prod_inv

added theorem measure_theory.measure_preserving_prod_inv_mul

added theorem measure_theory.measure_preserving_prod_inv_mul_swap

added theorem measure_theory.measure_preserving_prod_mul

added theorem measure_theory.measure_preserving_prod_mul_swap

modified theorem measure_theory.quasi_measure_preserving_mul_right

Modified src/measure_theory/measure/ae_measurable.lean

deleted theorem ae_measurable.comp_measurable'

added theorem ae_measurable.comp_quasi_measure_preserving

Modified src/measure_theory/measure/lebesgue.lean

Modified src/measure_theory/measure/measure_space.lean

added theorem measure_theory.measure.quasi_measure_preserving.ae_eq_comp