Commit 2023-07-28 12:48 3b522651

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...