feat: the Unfolding Trick (#6223)

This PR is a forward port of mathlib3 PR !3#18863

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



Co-authored-by: Matthew Ballard <matt@mrb.email>

Author: AlexKontorovich

Mathlib/GroupTheory/GroupAction/Group.lean

@@ -6,7 +6,7 @@ Authors: Chris Hughes
 import Mathlib.Algebra.Hom.Aut
 import Mathlib.GroupTheory.GroupAction.Units
 
-#align_import group_theory.group_action.group from "leanprover-community/mathlib"@"ba2245edf0c8bb155f1569fd9b9492a9b384cde6"
+#align_import group_theory.group_action.group from "leanprover-community/mathlib"@"3b52265189f3fb43aa631edffce5d060fafaf82f"
 
 /-!
 # Group actions applied to various types of group
@@ -265,6 +265,16 @@ def DistribMulAction.toAddAut : α →* AddAut β where
 #align distrib_mul_action.to_add_aut DistribMulAction.toAddAut
 #align distrib_mul_action.to_add_aut_apply DistribMulAction.toAddAut_apply
 
+/-- Each non-zero element of a `GroupWithZero` defines an additive monoid isomorphism of an
+`AddMonoid` on which it acts distributively.
+This is a stronger version of `DistribMulAction.toAddMonoidHom`. -/
+def DistribMulAction.toAddEquiv₀ {α : Type*} (β : Type*) [GroupWithZero α] [AddMonoid β]
+    [DistribMulAction α β] (x : α) (hx : x ≠ 0) : β ≃+ β :=
+  { DistribMulAction.toAddMonoidHom β x with
+    invFun := fun b ↦ x⁻¹ • b
+    left_inv := fun b ↦ inv_smul_smul₀ hx b
+    right_inv := fun b ↦ smul_inv_smul₀ hx b }
+
 variable {α β}
 
 theorem smul_eq_zero_iff_eq (a : α) {x : β} : a • x = 0 ↔ x = 0 :=

Mathlib/MeasureTheory/Group/FundamentalDomain.lean

@@ -6,7 +6,7 @@ Authors: Yury G. Kudryashov
 import Mathlib.MeasureTheory.Group.Action
 import Mathlib.MeasureTheory.Integral.SetIntegral
 
-#align_import measure_theory.group.fundamental_domain from "leanprover-community/mathlib"@"eb810cf549db839dadf13353dbe69bac55acdbbc"
+#align_import measure_theory.group.fundamental_domain from "leanprover-community/mathlib"@"3b52265189f3fb43aa631edffce5d060fafaf82f"
 
 /-!
 # Fundamental domain of a group action
@@ -253,6 +253,10 @@ theorem lintegral_eq_tsum' (h : IsFundamentalDomain G s μ) (f : α → ℝ≥0
 #align measure_theory.is_fundamental_domain.lintegral_eq_tsum' MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum'
 #align measure_theory.is_add_fundamental_domain.lintegral_eq_tsum' MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum'
 
+@[to_additive] lemma lintegral_eq_tsum'' (h : IsFundamentalDomain G s μ) (f : α → ℝ≥0∞) :
+    ∫⁻ x, f x ∂μ = ∑' g : G, ∫⁻ x in s, f (g • x) ∂μ :=
+  (lintegral_eq_tsum' h f).trans ((Equiv.inv G).tsum_eq (fun g ↦ ∫⁻ (x : α) in s, f (g • x) ∂μ))
+
 @[to_additive]
 theorem set_lintegral_eq_tsum (h : IsFundamentalDomain G s μ) (f : α → ℝ≥0∞) (t : Set α) :
     ∫⁻ x in t, f x ∂μ = ∑' g : G, ∫⁻ x in t ∩ g • s, f x ∂μ :=
@@ -426,6 +430,10 @@ theorem integral_eq_tsum' (h : IsFundamentalDomain G s μ) (f : α → E) (hf :
 #align measure_theory.is_fundamental_domain.integral_eq_tsum' MeasureTheory.IsFundamentalDomain.integral_eq_tsum'
 #align measure_theory.is_add_fundamental_domain.integral_eq_tsum' MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum'
 
+@[to_additive] lemma integral_eq_tsum'' (h : IsFundamentalDomain G s μ)
+    (f : α → E) (hf : Integrable f μ) : ∫ x, f x ∂μ = ∑' g : G, ∫ x in s, f (g • x) ∂μ :=
+  (integral_eq_tsum' h f hf).trans ((Equiv.inv G).tsum_eq (fun g ↦ ∫ (x : α) in s, f (g • x) ∂μ))
+
 @[to_additive]
 theorem set_integral_eq_tsum (h : IsFundamentalDomain G s μ) {f : α → E} {t : Set α}
     (hf : IntegrableOn f t μ) : ∫ x in t, f x ∂μ = ∑' g : G, ∫ x in t ∩ g • s, f x ∂μ :=

Mathlib/MeasureTheory/Measure/Haar/Quotient.lean

@@ -7,7 +7,7 @@ import Mathlib.MeasureTheory.Measure.Haar.Basic
 import Mathlib.MeasureTheory.Group.FundamentalDomain
 import Mathlib.Algebra.Group.Opposite
 
-#align_import measure_theory.measure.haar.quotient from "leanprover-community/mathlib"@"fd5edc43dc4f10b85abfe544b88f82cf13c5f844"
+#align_import measure_theory.measure.haar.quotient from "leanprover-community/mathlib"@"3b52265189f3fb43aa631edffce5d060fafaf82f"
 
 /-!
 # Haar quotient measure
@@ -34,7 +34,7 @@ Note that a group `G` with Haar measure that is both left and right invariant is
 
 open Set MeasureTheory TopologicalSpace MeasureTheory.Measure
 
-open scoped Pointwise NNReal
+open scoped Pointwise NNReal ENNReal
 
 variable {G : Type*} [Group G] [MeasurableSpace G] [TopologicalSpace G] [TopologicalGroup G]
   [BorelSpace G] {μ : Measure G} {Γ : Subgroup G}
@@ -113,16 +113,15 @@ theorem MeasureTheory.IsFundamentalDomain.isMulLeftInvariant_map [Subgroup.Norma
 #align measure_theory.is_fundamental_domain.is_mul_left_invariant_map MeasureTheory.IsFundamentalDomain.isMulLeftInvariant_map
 #align measure_theory.is_add_fundamental_domain.is_add_left_invariant_map MeasureTheory.IsAddFundamentalDomain.isAddLeftInvariant_map
 
-variable [T2Space (G ⧸ Γ)] [SecondCountableTopology (G ⧸ Γ)] (K : PositiveCompacts (G ⧸ Γ))
-
 /-- Given a normal subgroup `Γ` of a topological group `G` with Haar measure `μ`, which is also
   right-invariant, and a finite volume fundamental domain `𝓕`, the pushforward to the quotient
   group `G ⧸ Γ` of the restriction of `μ` to `𝓕` is a multiple of Haar measure on `G ⧸ Γ`. -/
 @[to_additive "Given a normal subgroup `Γ` of an additive topological group `G` with Haar measure
   `μ`, which is also right-invariant, and a finite volume fundamental domain `𝓕`, the pushforward
   to the quotient group `G ⧸ Γ` of the restriction of `μ` to `𝓕` is a multiple of Haar measure on
   `G ⧸ Γ`."]
-theorem MeasureTheory.IsFundamentalDomain.map_restrict_quotient [Subgroup.Normal Γ]
+theorem MeasureTheory.IsFundamentalDomain.map_restrict_quotient  [T2Space (G ⧸ Γ)]
+    [SecondCountableTopology (G ⧸ Γ)] (K : PositiveCompacts (G ⧸ Γ)) [Subgroup.Normal Γ]
     [MeasureTheory.Measure.IsHaarMeasure μ] [μ.IsMulRightInvariant] (h𝓕_finite : μ 𝓕 < ⊤) :
     Measure.map (QuotientGroup.mk' Γ) (μ.restrict 𝓕) =
       μ (𝓕 ∩ QuotientGroup.mk' Γ ⁻¹' K) • MeasureTheory.Measure.haarMeasure K := by
@@ -147,12 +146,167 @@ theorem MeasureTheory.IsFundamentalDomain.map_restrict_quotient [Subgroup.Normal
   topological group `G` with Haar measure `μ`, which is also right-invariant, and a finite volume
   fundamental domain `𝓕`, the quotient map to `G ⧸ Γ` is measure-preserving between appropriate
   multiples of Haar measure on `G` and `G ⧸ Γ`."]
-theorem MeasurePreservingQuotientGroup.mk' [Subgroup.Normal Γ]
-    [MeasureTheory.Measure.IsHaarMeasure μ] [μ.IsMulRightInvariant] (h𝓕_finite : μ 𝓕 < ⊤) (c : ℝ≥0)
+theorem MeasurePreservingQuotientGroup.mk' [T2Space (G ⧸ Γ)] [SecondCountableTopology (G ⧸ Γ)]
+    (K : PositiveCompacts (G ⧸ Γ)) [Subgroup.Normal Γ] [μ.IsHaarMeasure]
+    [μ.IsMulRightInvariant] (h𝓕_finite : μ 𝓕 < ⊤) (c : ℝ≥0)
     (h : μ (𝓕 ∩ QuotientGroup.mk' Γ ⁻¹' K) = c) :
     MeasurePreserving (QuotientGroup.mk' Γ) (μ.restrict 𝓕)
       (c • MeasureTheory.Measure.haarMeasure K) where
   measurable := continuous_quotient_mk'.measurable
   map_eq := by rw [h𝓕.map_restrict_quotient K h𝓕_finite, h]; rfl
 #align measure_preserving_quotient_group.mk' MeasurePreservingQuotientGroup.mk'
 #align measure_preserving_quotient_add_group.mk' MeasurePreservingQuotientAddGroup.mk'
+
+section
+
+local notation "μ_𝓕" => Measure.map (@QuotientGroup.mk G _ Γ) (μ.restrict 𝓕)
+
+/-- The `essSup` of a function `g` on the quotient space `G ⧸ Γ` with respect to the pushforward
+  of the restriction, `μ_𝓕`, of a right-invariant measure `μ` to a fundamental domain `𝓕`, is the
+  same as the `essSup` of `g`'s lift to the universal cover `G` with respect to `μ`. -/
+@[to_additive "The `essSup` of a function `g` on the additive quotient space `G ⧸ Γ` with respect
+  to the pushforward of the restriction, `μ_𝓕`, of a right-invariant measure `μ` to a fundamental
+  domain `𝓕`, is the same as the `essSup` of `g`'s lift to the universal cover `G` with respect
+  to `μ`."]
+lemma essSup_comp_quotientGroup_mk [μ.IsMulRightInvariant] {g : G ⧸ Γ → ℝ≥0∞}
+    (g_ae_measurable : AEMeasurable g μ_𝓕) : essSup g μ_𝓕 = essSup (fun (x : G) ↦ g x) μ := by
+  have hπ : Measurable (QuotientGroup.mk : G → G ⧸ Γ) := continuous_quotient_mk'.measurable
+  rw [essSup_map_measure g_ae_measurable hπ.aemeasurable]
+  refine h𝓕.essSup_measure_restrict ?_
+  intro ⟨γ, hγ⟩ x
+  dsimp
+  congr 1
+  exact QuotientGroup.mk_mul_of_mem x hγ
+
+/-- Given a quotient space `G ⧸ Γ` where `Γ` is `Countable`, and the restriction,
+  `μ_𝓕`, of a right-invariant measure `μ` on `G` to a fundamental domain `𝓕`, a set
+  in the quotient which has `μ_𝓕`-measure zero, also has measure zero under the
+  folding of `μ` under the quotient. Note that, if `Γ` is infinite, then the folded map
+  will take the value `∞` on any open set in the quotient! -/
+@[to_additive "Given an additive quotient space `G ⧸ Γ` where `Γ` is `Countable`, and the
+  restriction, `μ_𝓕`, of a right-invariant measure `μ` on `G` to a fundamental domain `𝓕`, a set
+  in the quotient which has `μ_𝓕`-measure zero, also has measure zero under the
+  folding of `μ` under the quotient. Note that, if `Γ` is infinite, then the folded map
+  will take the value `∞` on any open set in the quotient!"]
+lemma _root_.MeasureTheory.IsFundamentalDomain.absolutelyContinuous_map
+    [μ.IsMulRightInvariant] :
+    map (QuotientGroup.mk : G → G ⧸ Γ) μ ≪ map (QuotientGroup.mk : G → G ⧸ Γ) (μ.restrict 𝓕) := by
+  set π : G → G ⧸ Γ := QuotientGroup.mk
+  have meas_π : Measurable π := continuous_quotient_mk'.measurable
+  apply AbsolutelyContinuous.mk
+  intro s s_meas hs
+  rw [map_apply meas_π s_meas] at hs ⊢
+  rw [Measure.restrict_apply] at hs
+  apply h𝓕.measure_zero_of_invariant _ _ hs
+  · intro γ
+    ext g
+    rw [Set.mem_smul_set_iff_inv_smul_mem, mem_preimage, mem_preimage]
+    congr! 1
+    convert QuotientGroup.mk_mul_of_mem g (γ⁻¹).2 using 1
+  exact MeasurableSet.preimage s_meas meas_π
+
+attribute [-instance] Quotient.instMeasurableSpace
+
+/-- This is a simple version of the **Unfolding Trick**: 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 quotient `G ⧸ Γ` of the automorphization of `f`. -/
+@[to_additive "This is a simple version of the **Unfolding Trick**: Given a subgroup `Γ` of an
+  additive  group `G`, the integral of a function `f` on `G` with respect to a right-invariant
+  measure `μ` is equal to the integral over the quotient `G ⧸ Γ` of the automorphization of `f`."]
+lemma QuotientGroup.integral_eq_integral_automorphize {E : Type*} [NormedAddCommGroup E]
+    [NormedSpace ℝ E] [μ.IsMulRightInvariant] {f : G → E}
+    (hf₁ : Integrable f μ) (hf₂ : AEStronglyMeasurable (automorphize f) μ_𝓕) :
+    ∫ x : G, f x ∂μ = ∫ x : G ⧸ Γ, automorphize f x ∂μ_𝓕 := by
+  calc ∫ x : G, f x ∂μ = ∑' γ : (Subgroup.opposite Γ), ∫ x in 𝓕, f (γ • x) ∂μ :=
+    h𝓕.integral_eq_tsum'' f hf₁
+    _ = ∫ x in 𝓕, ∑' γ : (Subgroup.opposite Γ), f (γ • x) ∂μ := ?_
+    _ = ∫ x : G ⧸ Γ, automorphize f x ∂μ_𝓕 :=
+      (integral_map continuous_quotient_mk'.aemeasurable hf₂).symm
+  rw [integral_tsum]
+  · exact fun i ↦ (hf₁.1.comp_quasiMeasurePreserving
+      (measurePreserving_smul i μ).quasiMeasurePreserving).restrict
+  · rw [← h𝓕.lintegral_eq_tsum'' (fun x ↦ ‖f x‖₊)]
+    exact ne_of_lt hf₁.2
+
+/-- This is 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 quotient `G ⧸ Γ` with respect
+  to a right-invariant measure `μ` on `G`, is equal to the integral over the quotient of the
+  automorphization of `f` times `g`. -/
+lemma QuotientGroup.integral_mul_eq_integral_automorphize_mul {K : Type*} [NormedField K]
+    [NormedSpace ℝ K] [μ.IsMulRightInvariant] {f : G → K}
+    (f_ℒ_1 : Integrable f μ) {g : G ⧸ Γ → K} (hg : AEStronglyMeasurable g μ_𝓕)
+    (g_ℒ_infinity : essSup (fun x ↦ ↑‖g x‖₊) μ_𝓕 ≠ ∞)
+    (F_ae_measurable : AEStronglyMeasurable (QuotientGroup.automorphize f) μ_𝓕) :
+    ∫ x : G, g (x : G ⧸ Γ) * (f x) ∂μ
+      = ∫ x : G ⧸ Γ, g x * (QuotientGroup.automorphize f x) ∂μ_𝓕 := by
+  let π : G → G ⧸ Γ := QuotientGroup.mk
+  have meas_π : Measurable π := continuous_quotient_mk'.measurable
+  have H₀ : QuotientGroup.automorphize ((g ∘ π) * f) = g * (QuotientGroup.automorphize f) := by
+    exact QuotientGroup.automorphize_smul_left f g
+  calc ∫ (x : G), g (π x) * (f x) ∂μ =
+        ∫ (x : G ⧸ Γ), QuotientGroup.automorphize ((g ∘ π) * f) x ∂μ_𝓕 := ?_
+    _ = ∫ (x : G ⧸ Γ), g x * (QuotientGroup.automorphize f x) ∂μ_𝓕 := by simp [H₀]
+  have H₁ : Integrable ((g ∘ π) * f) μ
+  · have : AEStronglyMeasurable (fun (x : G) ↦ g (x : (G ⧸ Γ))) μ
+    · refine (AEStronglyMeasurable.mono' hg ?_).comp_measurable meas_π
+      exact h𝓕.absolutelyContinuous_map
+    refine Integrable.essSup_smul f_ℒ_1 this ?_
+    have hg' : AEStronglyMeasurable (fun x ↦ (‖g x‖₊ : ℝ≥0∞)) μ_𝓕 :=
+      (ENNReal.continuous_coe.comp continuous_nnnorm).comp_aestronglyMeasurable hg
+    rw [← essSup_comp_quotientGroup_mk h𝓕 hg'.aemeasurable]
+    exact g_ℒ_infinity
+  have H₂ : AEStronglyMeasurable (QuotientGroup.automorphize ((g ∘ π) * f)) μ_𝓕
+  · simp_rw [H₀]
+    exact hg.mul F_ae_measurable
+  apply QuotientGroup.integral_eq_integral_automorphize h𝓕 H₁ H₂
+
+end
+
+section
+
+variable {G' : Type*} [AddGroup G'] [MeasurableSpace G'] [TopologicalSpace G']
+  [TopologicalAddGroup G'] [BorelSpace G']
+  {μ' : Measure G'}
+  {Γ' : AddSubgroup G'}
+  [Countable Γ'] [MeasurableSpace (G' ⧸ Γ')] [BorelSpace (G' ⧸ Γ')]
+  {𝓕' : Set G'}
+
+local notation "μ_𝓕" => Measure.map (@QuotientAddGroup.mk G' _ Γ') (μ'.restrict 𝓕')
+
+/-- This is the **Unfolding Trick**: Given an additive subgroup `Γ'` of an additive group `G'`, the
+  integral of a function `f` on `G'` times the lift to `G'` of a function `g` on the quotient
+  `G' ⧸ Γ'` with respect to a right-invariant measure `μ` on `G'`, is equal to the integral over
+  the quotient of the automorphization of `f` times `g`. -/
+lemma QuotientAddGroup.integral_mul_eq_integral_automorphize_mul {K : Type*} [NormedField K]
+    [NormedSpace ℝ K] [μ'.IsAddRightInvariant] {f : G' → K}
+    (f_ℒ_1 : Integrable f μ') {g : G' ⧸ Γ' → K} (hg : AEStronglyMeasurable g μ_𝓕)
+    (g_ℒ_infinity : essSup (fun x ↦ (‖g x‖₊ : ℝ≥0∞)) μ_𝓕 ≠ ∞)
+    (F_ae_measurable : AEStronglyMeasurable (QuotientAddGroup.automorphize f) μ_𝓕)
+    (h𝓕 : IsAddFundamentalDomain (AddSubgroup.opposite Γ') 𝓕' μ') :
+    ∫ x : G', g (x : G' ⧸ Γ') * (f x) ∂μ'
+      = ∫ x : G' ⧸ Γ', g x * (QuotientAddGroup.automorphize f x) ∂μ_𝓕 := by
+  let π : G' → G' ⧸ Γ' := QuotientAddGroup.mk
+  have meas_π : Measurable π := continuous_quotient_mk'.measurable
+  have H₀ : QuotientAddGroup.automorphize ((g ∘ π) * f) = g * (QuotientAddGroup.automorphize f) :=
+    by exact QuotientAddGroup.automorphize_smul_left f g
+  calc ∫ (x : G'), g (π x) * f x ∂μ' =
+    ∫ (x : G' ⧸ Γ'), QuotientAddGroup.automorphize ((g ∘ π) * f) x ∂μ_𝓕 := ?_
+    _ = ∫ (x : G' ⧸ Γ'), g x * (QuotientAddGroup.automorphize f x) ∂μ_𝓕 := by simp [H₀]
+  have H₁ : Integrable ((g ∘ π) * f) μ'
+  · have : AEStronglyMeasurable (fun (x : G') ↦ g (x : (G' ⧸ Γ'))) μ'
+    · refine (AEStronglyMeasurable.mono' hg ?_).comp_measurable meas_π
+      exact h𝓕.absolutelyContinuous_map
+    refine Integrable.essSup_smul f_ℒ_1 this ?_
+    have hg' : AEStronglyMeasurable (fun x ↦ (‖g x‖₊ : ℝ≥0∞)) μ_𝓕 :=
+      (ENNReal.continuous_coe.comp continuous_nnnorm).comp_aestronglyMeasurable hg
+    rw [← essSup_comp_quotientAddGroup_mk h𝓕 hg'.aemeasurable]
+    exact g_ℒ_infinity
+  have H₂ : AEStronglyMeasurable (QuotientAddGroup.automorphize ((g ∘ π) * f)) μ_𝓕
+  · simp_rw [H₀]
+    exact hg.mul F_ae_measurable
+  apply QuotientAddGroup.integral_eq_integral_automorphize h𝓕 H₁ H₂
+
+end
+
+attribute [to_additive existing QuotientGroup.integral_mul_eq_integral_automorphize_mul]
+  QuotientAddGroup.integral_mul_eq_integral_automorphize_mul