We prove the "unfolding trick": Given a subgroup `Γ` of a group `G`, the integral of a function `f` on `G` times the lift to `G` of a function `g` on the coset space `G ⧸ Γ` with respect to a right-invariant measure `μ` on `G`, is equal to the integral over the coset space of the automorphization of `f` times `g`.

We also prove the following simplified version: Given a subgroup `Γ` of a group `G`, the integral of a function `f` on `G` with respect to a right-invariant measure `μ` is equal to the integral over the coset space `G ⧸ Γ` of the automorphization of `f`.

A question: is it possible to deduce `ae_strongly_measurable (quotient_group.automorphize f) μ_𝓕` from `ae_strongly_measurable f μ` (as opposed to assuming it as a hypothesis in the main theorem)? It seems quite plausible...

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



Co-authored-by: Alex Kontorovich <58564076+AlexKontorovich@users.noreply.github.com>
Co-authored-by: AlexKontorovich <58564076+AlexKontorovich@users.noreply.github.com>

…nuous measures (#10564)

Rename `AEStronglyMeasurable.mono'` to `AEStronglyMeasurable.mono_ac`.

Partly forward-port leanprover-community/mathlib3#18863



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

…nuous measures (#10564)

Rename `AEStronglyMeasurable.mono'` to `AEStronglyMeasurable.mono_ac`.

Partly forward-port leanprover-community/mathlib3#18863



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

…nuous measures (#10564)

Rename `AEStronglyMeasurable.mono'` to `AEStronglyMeasurable.mono_ac`.

Partly forward-port leanprover-community/mathlib3#18863



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

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>

* commit '65a1391a0106c9204fe45bc73a039f056558cb83': (12443 commits)
  feat(data/{list,multiset,finset}/*): `attach` and `filter` lemmas (leanprover-community#18087)
  feat(combinatorics/simple_graph): More clique lemmas (leanprover-community#19203)
  feat(measure_theory/order/upper_lower): Order-connected sets in `ℝⁿ` are measurable (leanprover-community#16976)
  move old README.md to OLD_README.md
  doc: Add a warning mentioning Lean 4 to the readme (leanprover-community#19243)
  feat(topology/metric_space): diameter of pointwise zero and addition (leanprover-community#19028)
  feat(topology/algebra/order/liminf_limsup): Eventual boundedness of neighborhoods (leanprover-community#18629)
  feat(probability/independence): Independence of singletons (leanprover-community#18506)
  feat(combinatorics/set_family/ahlswede_zhang): Ahlswede-Zhang identity, part I (leanprover-community#18612)
  feat(data/finset/lattice): `sup'`/`inf'` lemmas (leanprover-community#18989)
  chore(order/liminf_limsup): Generalise and move lemmas (leanprover-community#18628)
  feat(algebraic_topology/dold_kan): The Dold-Kan equivalence for abelian categories (leanprover-community#17926)
  feat(data/sum/interval): The lexicographic sum of two locally finite orders is locally finite (leanprover-community#11352)
  feat(analysis/convex/proj_Icc): Extending convex functions (leanprover-community#18797)
  feat(algebraic_topology/dold_kan): The Dold-Kan equivalence for pseudoabelian categories (leanprover-community#17925)
  feat(measure_theory/measure/haar_quotient): the Unfolding Trick (leanprover-community#18863)
  feat(linear_algebra/orientation): add `orientation.reindex` (leanprover-community#19236)
  feat(combinatorics/quiver/covering): Definition of coverings and unique lifting of paths (leanprover-community#17828)
  feat(set_theory/game/pgame): small sets of pre-games / games / surreals are bounded (leanprover-community#15260)
  feat(tactic/positivity): Extension for `ite` (leanprover-community#17650)
  ...

# Conflicts:
#	README.md