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 leanprover-community/mathlib3#18863

Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>



Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>

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 leanprover-community/mathlib3#18863

Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>



Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>

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 leanprover-community/mathlib3#18863

Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>



Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>

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 leanprover-community/mathlib3#18863

Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>



Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>

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 leanprover-community/mathlib3#18863

Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>



Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>