feat(measure_theory/measure/haar_quotient): Pushforward of Haar measu…

…re is Haar (#11593)

For `G` a topological group with discrete subgroup `Γ`, the pushforward to the coset space `G ⧸ Γ` of the restriction of a both left- and right-invariant measure on `G` to a fundamental domain `𝓕` is a `G`-invariant measure on `G ⧸ Γ`. When `Γ` is normal (and under other certain suitable conditions), we show that this measure is the Haar measure on the quotient group `G ⧸ Γ`.

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



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

src/group_theory/subgroup/basic.lean

@@ -2661,6 +2661,44 @@ end subgroup
 
 end actions
 
+/-! ### Mul-opposite subgroups -/
+
+section mul_opposite
+
+namespace subgroup
+
+/-- A subgroup `H` of `G` determines a subgroup `H.opposite` of the opposite group `Gᵐᵒᵖ`. -/
+@[to_additive "An additive subgroup `H` of `G` determines an additive subgroup `H.opposite` of the
+  opposite additive group `Gᵃᵒᵖ`."]
+def opposite (H : subgroup G) : subgroup Gᵐᵒᵖ :=
+{ carrier := mul_opposite.unop ⁻¹' (H : set G),
+  one_mem' := H.one_mem,
+  mul_mem' := λ a b ha hb, H.mul_mem hb ha,
+  inv_mem' := λ a, H.inv_mem }
+
+/-- Bijection between a subgroup `H` and its opposite. -/
+@[to_additive "Bijection between an additive subgroup `H` and its opposite.", simps]
+def opposite_equiv (H : subgroup G) : H ≃ H.opposite :=
+mul_opposite.op_equiv.subtype_equiv $ λ _, iff.rfl
+
+@[to_additive] instance (H : subgroup G) [encodable H] : encodable H.opposite :=
+encodable.of_equiv H H.opposite_equiv.symm
+
+@[to_additive] lemma smul_opposite_mul {H : subgroup G} (x g : G) (h : H.opposite) :
+  h • (g * x) = g * (h • x) :=
+begin
+  cases h,
+  simp [(•), mul_assoc],
+end
+
+@[to_additive] lemma smul_opposite_image_mul_preimage {H : subgroup G} (g : G) (h : H.opposite)
+  (s : set G) : (λ y, h • y) '' (has_mul.mul g ⁻¹' s) = has_mul.mul g ⁻¹' ((λ y, h • y) '' s) :=
+by { ext x, cases h, simp [(•), mul_assoc] }
+
+end subgroup
+
+end mul_opposite
+
 /-! ### Saturated subgroups -/
 
 section saturated

src/measure_theory/group/arithmetic.lean

@@ -577,29 +577,36 @@ end mul_action
 section opposite
 open mul_opposite
 
+@[to_additive]
 instance {α : Type*} [h : measurable_space α] : measurable_space αᵐᵒᵖ := measurable_space.map op h
 
-lemma measurable_op {α : Type*} [measurable_space α] : measurable (op : α → αᵐᵒᵖ) := λ s, id
+@[to_additive]
+lemma measurable_mul_op {α : Type*} [measurable_space α] : measurable (op : α → αᵐᵒᵖ) := λ s, id
 
-lemma measurable_unop {α : Type*} [measurable_space α] : measurable (unop : αᵐᵒᵖ → α) := λ s, id
+@[to_additive]
+lemma measurable_mul_unop {α : Type*} [measurable_space α] : measurable (unop : αᵐᵒᵖ → α) := λ s, id
 
+@[to_additive]
 instance {M : Type*} [has_mul M] [measurable_space M] [has_measurable_mul M] :
   has_measurable_mul Mᵐᵒᵖ :=
-⟨λ c, measurable_op.comp (measurable_unop.mul_const _),
-  λ c, measurable_op.comp (measurable_unop.const_mul _)⟩
+⟨λ c, measurable_mul_op.comp (measurable_mul_unop.mul_const _),
+  λ c, measurable_mul_op.comp (measurable_mul_unop.const_mul _)⟩
 
+@[to_additive]
 instance {M : Type*} [has_mul M] [measurable_space M] [has_measurable_mul₂ M] :
   has_measurable_mul₂ Mᵐᵒᵖ :=
-⟨measurable_op.comp ((measurable_unop.comp measurable_snd).mul
-  (measurable_unop.comp measurable_fst))⟩
+⟨measurable_mul_op.comp ((measurable_mul_unop.comp measurable_snd).mul
+  (measurable_mul_unop.comp measurable_fst))⟩
 
+@[to_additive]
 instance has_measurable_smul_opposite_of_mul {M : Type*} [has_mul M] [measurable_space M]
   [has_measurable_mul M] : has_measurable_smul Mᵐᵒᵖ M :=
-⟨λ c, measurable_mul_const (unop c), λ x, measurable_unop.const_mul x⟩
+⟨λ c, measurable_mul_const (unop c), λ x, measurable_mul_unop.const_mul x⟩
 
+@[to_additive]
 instance has_measurable_smul₂_opposite_of_mul {M : Type*} [has_mul M] [measurable_space M]
   [has_measurable_mul₂ M] : has_measurable_smul₂ Mᵐᵒᵖ M :=
-⟨measurable_snd.mul (measurable_unop.comp measurable_fst)⟩
+⟨measurable_snd.mul (measurable_mul_unop.comp measurable_fst)⟩
 
 end opposite
 

src/measure_theory/group/fundamental_domain.lean

@@ -152,6 +152,19 @@ calc ∫⁻ x in s, f x ∂μ = ∑' g : G, ∫⁻ x in s ∩ g • t, f x ∂μ
 ... = ∫⁻ x in t, f x ∂μ :
   (hs.set_lintegral_eq_tsum _ _).symm
 
+@[to_additive] lemma measure_set_eq (hs : is_fundamental_domain G s μ)
+  (ht : is_fundamental_domain G t μ) {A : set α} (hA₀ : measurable_set A)
+  (hA : ∀ (g : G), (λ x, g • x) ⁻¹' A = A) :
+  μ (A ∩ s) = μ (A ∩ t) :=
+begin
+  have : ∫⁻ x in s, A.indicator 1 x ∂μ = ∫⁻ x in t, A.indicator 1 x ∂μ,
+  { refine hs.set_lintegral_eq ht (set.indicator A (λ _, 1)) _,
+    intros g x,
+    convert (set.indicator_comp_right (λ x : α, g • x)).symm,
+    rw hA g },
+  simpa [measure.restrict_apply hA₀, lintegral_indicator _ hA₀] using this
+end
+
 /-- If `s` and `t` are two fundamental domains of the same action, then their measures are equal. -/
 @[to_additive] protected lemma measure_eq (hs : is_fundamental_domain G s μ)
   (ht : is_fundamental_domain G t μ) : μ s = μ t :=

src/measure_theory/measure/haar_quotient.lean

@@ -0,0 +1,183 @@
+/-
+Copyright (c) 2022 Alex Kontorovich and Heather Macbeth. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alex Kontorovich, Heather Macbeth
+-/
+
+import measure_theory.measure.haar
+import measure_theory.group.fundamental_domain
+import topology.compact_open
+import algebra.group.opposite
+
+/-!
+# Haar quotient measure
+
+In this file, we consider properties of fundamental domains and measures for the action of a
+subgroup of a group `G` on `G` itself.
+
+## Main results
+
+* `measure_theory.is_fundamental_domain.smul_invariant_measure_map `: given a subgroup `Γ` of a
+  topological group `G`, the pushforward to the coset space `G ⧸ Γ` of the restriction of a both
+  left- and right-invariant measure on `G` to a fundamental domain `𝓕` is a `G`-invariant measure
+  on `G ⧸ Γ`.
+
+* `measure_theory.is_fundamental_domain.is_mul_left_invariant_map `: given a normal subgroup `Γ` of
+  a topological group `G`, the pushforward to the quotient group `G ⧸ Γ` of the restriction of
+  a both left- and right-invariant measure on `G` to a fundamental domain `𝓕` is a left-invariant
+  measure on `G ⧸ Γ`.
+
+Note that a group `G` with Haar measure that is both left and right invariant is called
+**unimodular**.
+-/
+
+open set measure_theory topological_space measure_theory.measure
+
+variables {G : Type*} [group G] [measurable_space G] [topological_space G]
+  [topological_group G] [borel_space G]
+  {μ : measure G}
+  {Γ : subgroup G}
+
+/-- Given a subgroup `Γ` of `G` and a right invariant measure `μ` on `G`, the measure is also
+  invariant under the action of `Γ` on `G` by **right** multiplication. -/
+@[to_additive "Given a subgroup `Γ` of an additive group `G` and a right invariant measure `μ` on
+  `G`, the measure is also invariant under the action of `Γ` on `G` by **right** addition."]
+lemma subgroup.smul_invariant_measure [μ.is_mul_right_invariant] :
+  smul_invariant_measure Γ.opposite G μ :=
+{ measure_preimage_smul :=
+begin
+  rintros ⟨c, hc⟩ s hs,
+  dsimp [(•)],
+  refine measure_preimage_mul_right μ (mul_opposite.unop c) s,
+end}
+
+/-- Measurability of the action of the topological group `G` on the left-coset space `G/Γ`. -/
+@[to_additive "Measurability of the action of the additive topological group `G` on the left-coset
+  space `G/Γ`."]
+instance quotient_group.has_measurable_smul [measurable_space (G ⧸ Γ)] [borel_space (G ⧸ Γ)] :
+  has_measurable_smul G (G ⧸ Γ) :=
+{ measurable_const_smul := λ g, (continuous_const_smul g).measurable,
+  measurable_smul_const := λ x, (quotient_group.continuous_smul₁ x).measurable }
+
+variables {𝓕 : set G} (h𝓕 : is_fundamental_domain Γ.opposite 𝓕 μ)
+include h𝓕
+
+/-- If `𝓕` is a fundamental domain for the action by right multiplication of a subgroup `Γ` of a
+  topological group `G`, then its left-translate by an element of `g` is also a fundamental
+  domain. -/
+@[to_additive "If `𝓕` is a fundamental domain for the action by right addition of a subgroup `Γ`
+  of an additive topological group `G`, then its left-translate by an element of `g` is also a
+  fundamental domain."]
+lemma measure_theory.is_fundamental_domain.smul (g : G) [μ.is_mul_left_invariant] :
+  is_fundamental_domain ↥Γ.opposite (has_mul.mul g ⁻¹' 𝓕) μ :=
+{ measurable_set := measurable_set_preimage (measurable_const_mul g) (h𝓕.measurable_set),
+  ae_covers := begin
+    let s := {x : G | ¬∃ (γ : ↥(Γ.opposite)), γ • x ∈ 𝓕},
+    have μs_eq_zero : μ s = 0 := h𝓕.2,
+    change μ {x : G | ¬∃ (γ : ↥(Γ.opposite)), g * γ • x ∈ 𝓕} = 0,
+    have : {x : G | ¬∃ (γ : ↥(Γ.opposite)), g * γ • x ∈ 𝓕} = has_mul.mul g ⁻¹' s,
+    { ext,
+      simp [s, subgroup.smul_opposite_mul], },
+    rw [this, measure_preimage_mul μ g s, μs_eq_zero],
+  end,
+  ae_disjoint := begin
+    intros γ γ_ne_one,
+    have μs_eq_zero : μ (((λ x, γ • x) '' 𝓕) ∩ 𝓕) = 0 := h𝓕.3 γ γ_ne_one,
+    change μ (((λ x, γ • x) '' (has_mul.mul g ⁻¹' 𝓕)) ∩ (has_mul.mul g ⁻¹' 𝓕)) = 0,
+    rw [subgroup.smul_opposite_image_mul_preimage, ← preimage_inter, measure_preimage_mul μ g _,
+      μs_eq_zero],
+  end }
+
+variables [encodable Γ] [measurable_space (G ⧸ Γ)] [borel_space (G ⧸ Γ)]
+
+/-- The pushforward to the coset space `G ⧸ Γ` of the restriction of a both left- and right-
+  invariant measure on `G` to a fundamental domain `𝓕` is a `G`-invariant measure on `G ⧸ Γ`. -/
+@[to_additive "The pushforward to the coset space `G ⧸ Γ` of the restriction of a both left- and
+  right-invariant measure on an additive topological group `G` to a fundamental domain `𝓕` is a
+  `G`-invariant measure on `G ⧸ Γ`."]
+lemma measure_theory.is_fundamental_domain.smul_invariant_measure_map
+  [μ.is_mul_left_invariant] [μ.is_mul_right_invariant] :
+  smul_invariant_measure G (G ⧸ Γ) (measure.map quotient_group.mk (μ.restrict 𝓕)) :=
+{ measure_preimage_smul :=
+  begin
+    let π : G → G ⧸ Γ := quotient_group.mk,
+    have meas_π : measurable π :=
+      continuous_quotient_mk.measurable,
+    have 𝓕meas : measurable_set 𝓕 := h𝓕.measurable_set,
+    intros g A hA,
+    have meas_πA : measurable_set (π ⁻¹' A) := measurable_set_preimage meas_π hA,
+    rw [measure.map_apply meas_π hA,
+      measure.map_apply meas_π (measurable_set_preimage (measurable_const_smul g) hA),
+      measure.restrict_apply' 𝓕meas, measure.restrict_apply' 𝓕meas],
+    set π_preA := π ⁻¹' A,
+    have : (quotient_group.mk ⁻¹' ((λ (x : G ⧸ Γ), g • x) ⁻¹' A)) = has_mul.mul g ⁻¹' π_preA,
+    { ext1, simp },
+    rw this,
+    have : μ (has_mul.mul g ⁻¹' π_preA ∩ 𝓕) = μ (π_preA ∩ has_mul.mul (g⁻¹) ⁻¹' 𝓕),
+    { transitivity μ (has_mul.mul g ⁻¹' (π_preA ∩ has_mul.mul g⁻¹ ⁻¹' 𝓕)),
+      { rw preimage_inter,
+        congr,
+        rw [← preimage_comp, comp_mul_left, mul_left_inv],
+        ext,
+        simp, },
+      rw measure_preimage_mul, },
+    rw this,
+    have h𝓕_translate_fundom : is_fundamental_domain Γ.opposite (has_mul.mul g⁻¹ ⁻¹' 𝓕) μ :=
+      h𝓕.smul (g⁻¹),
+    haveI : smul_invariant_measure ↥(Γ.opposite) G μ := subgroup.smul_invariant_measure,
+    rw h𝓕.measure_set_eq h𝓕_translate_fundom meas_πA,
+    rintros ⟨γ, γ_in_Γ⟩,
+    ext,
+    have : π (x * (mul_opposite.unop γ)) = π (x) := by simpa [quotient_group.eq'] using γ_in_Γ,
+    simp [(•), this],
+  end }
+
+/-- Assuming `Γ` is a normal subgroup of a topological group `G`, the pushforward to the quotient
+  group `G ⧸ Γ` of the restriction of a both left- and right-invariant measure on `G` to a
+  fundamental domain `𝓕` is a left-invariant measure on `G ⧸ Γ`. -/
+@[to_additive "Assuming `Γ` is a normal subgroup of an additive topological group `G`, the
+  pushforward to the quotient group `G ⧸ Γ` of the restriction of a both left- and right-invariant
+  measure on `G` to a fundamental domain `𝓕` is a left-invariant measure on `G ⧸ Γ`."]
+lemma measure_theory.is_fundamental_domain.is_mul_left_invariant_map [subgroup.normal Γ]
+  [μ.is_mul_left_invariant] [μ.is_mul_right_invariant] :
+  (measure.map (quotient_group.mk' Γ) (μ.restrict 𝓕)).is_mul_left_invariant :=
+{ map_mul_left_eq_self := begin
+    intros x,
+    apply measure.ext,
+    intros A hA,
+    obtain ⟨x₁, _⟩ := @quotient.exists_rep _ (quotient_group.left_rel Γ) x,
+    haveI := h𝓕.smul_invariant_measure_map,
+    convert measure_preimage_smul x₁ ((measure.map quotient_group.mk) (μ.restrict 𝓕)) A using 1,
+    rw [← h, measure.map_apply],
+    { refl, },
+    { exact measurable_const_mul _, },
+    { exact hA, },
+  end }
+
+variables [t2_space (G ⧸ Γ)] [second_countable_topology (G ⧸ Γ)] (K : positive_compacts (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 ⧸ Γ`."]
+lemma measure_theory.is_fundamental_domain.map_restrict_quotient [subgroup.normal Γ]
+  [measure_theory.measure.is_haar_measure μ] [μ.is_mul_right_invariant]
+  (h𝓕_finite : μ 𝓕 < ⊤) : measure.map (quotient_group.mk' Γ) (μ.restrict 𝓕)
+  = (μ (𝓕 ∩ (quotient_group.mk' Γ) ⁻¹' K.val)) • (measure_theory.measure.haar_measure K) :=
+begin
+  let π : G →* G ⧸ Γ := quotient_group.mk' Γ,
+  have meas_π : measurable π := continuous_quotient_mk.measurable,
+  have 𝓕meas : measurable_set 𝓕 := h𝓕.measurable_set,
+  haveI : is_finite_measure (μ.restrict 𝓕) :=
+    ⟨by { rw [measure.restrict_apply' 𝓕meas, univ_inter], exact h𝓕_finite }⟩,
+  -- the measure is left-invariant, so by the uniqueness of Haar measure it's enough to show that
+  -- it has the stated size on the reference compact set `K`.
+  haveI : (measure.map (quotient_group.mk' Γ) (μ.restrict 𝓕)).is_mul_left_invariant :=
+    h𝓕.is_mul_left_invariant_map,
+  rw [measure.haar_measure_unique (measure.map (quotient_group.mk' Γ) (μ.restrict 𝓕)) K,
+    measure.map_apply meas_π, measure.restrict_apply' 𝓕meas, inter_comm],
+  exact K.prop.1.measurable_set,
+end