Commit 2024-11-12 10:47 4212997a

View on Github →

feat(MeasureTheory): prove that some equivalences are measure preserving (#17944) Construct measurable equivalence for the following equiv and then prove that they are measure preserving:

Equiv.arrowProdEquivProdArrow
Equiv.arrowCongr'
Equiv.prodAssoc Also, we fix a typo in MeasureTheory.measurePreserving_pi This PR is part of the proof of the Analytic Class Number Formula.

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/Pi.lean

added theorem MeasureTheory.measurePreserving_arrowCongr'

added theorem MeasureTheory.measurePreserving_arrowProdEquivProdArrow

added theorem MeasureTheory.volume_measurePreserving_arrowProdEquivProdArrow

added theorem MeasureTheory.volume_preserving_arrowCongr'

Modified Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean

added def MeasurableEquiv.arrowCongr'

added def MeasurableEquiv.arrowProdEquivProdArrow

Modified Mathlib/MeasureTheory/Measure/Prod.lean

added theorem MeasureTheory.measurePreserving_prodAssoc

added theorem MeasureTheory.volume_preserving_prodAssoc