Commit 2024-04-05 21:50 fea58cd7

refactor: typeclasses for measures on quotient spaces and groups (#7506) We introduce a new typeclass QuotientMeasureEqMeasurePreimage which expresses a relationship between a measure on a space and a measure on its quotient under a discrete group action. Namely, the volume of a measurable set in the quotient is equal to the volume of its preimage, intersected with any fundamental domain. Our main application is in the context of a discrete normal subgroup of a topological group acting on the group itself, so as to compare Haar measures on a group and its quotient. Before this typeclass, you could have Haar measure upstairs and downstairs and you would have ugly scaling factors if you wanted to compare the two. This typeclass more accurately reflects what is needed in order to have a clear relationship between the upstairs and downstairs measures. Two big theorems (proved under various technical assumptions, like finiteness of the volume - which shouldn't be necessary): (1) if you're Haar upstairs and satisfy QuotientMeasureEqMeasurePreimage, then you're Haar downstairs. And conversely (2): if you're Haar upstairs and downstairs, and scale correctly on a single measurable set, then you satisfy QuotientMeasureEqMeasurePreimage. Contains the forward-port of https://github.com/leanprover-community/mathlib/pull/18863