mathlib

3b522651 - feat(measure_theory/measure/haar_quotient): the Unfolding Trick (#18863)

feat(measure_theory/measure/haar_quotient): the Unfolding Trick (#18863) 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>