refactor(measure_theory/group/fundamental_domain): Use pairwise (#17928)

Replace `∀ g ≠ (1 : G), ae_disjoint μ (g • s) s` ("translates are disjoint to the original set") by the stronger and more symmetric `pairwise (ae_disjoint μ on λ g : G, g • s)` ("translates are disjoint"). In full generality, the latter condition is the one we mean, and indeed this change reduces typeclass assumptions for a few lemmas.

Author: YaelDillies

src/measure_theory/group/fundamental_domain.lean

@@ -38,7 +38,7 @@ a.e. disjoint and cover the whole space. -/
   [has_vadd G α] [measurable_space α] (s : set α) (μ : measure α . volume_tac) : Prop :=
 (null_measurable_set : null_measurable_set s μ)
 (ae_covers : ∀ᵐ x ∂μ, ∃ g : G, g +ᵥ x ∈ s)
-(ae_disjoint : ∀ g ≠ (0 : G), ae_disjoint μ (g +ᵥ s) s)
+(ae_disjoint : pairwise $ ae_disjoint μ on λ g : G, g +ᵥ s)
 
 /-- A measurable set `s` is a *fundamental domain* for an action of a group `G` on a measurable
 space `α` with respect to a measure `α` if the sets `g • s`, `g : G`, are pairwise a.e. disjoint and
@@ -48,12 +48,13 @@ structure is_fundamental_domain (G : Type*) {α : Type*} [has_one G] [has_smul G
   [measurable_space α] (s : set α) (μ : measure α . volume_tac) : Prop :=
 (null_measurable_set : null_measurable_set s μ)
 (ae_covers : ∀ᵐ x ∂μ, ∃ g : G, g • x ∈ s)
-(ae_disjoint : ∀ g ≠ (1 : G), ae_disjoint μ (g • s) s)
+(ae_disjoint : pairwise $ ae_disjoint μ on λ g : G, g • s)
 
-namespace is_fundamental_domain
+variables {G H α β E : Type*}
 
-variables {G H α β E : Type*} [group G] [group H] [mul_action G α] [measurable_space α]
-  [mul_action H β] [measurable_space β] [normed_add_comm_group E] {s t : set α} {μ : measure α}
+namespace is_fundamental_domain
+variables [group G] [group H] [mul_action G α] [measurable_space α] [mul_action H β]
+  [measurable_space β] [normed_add_comm_group E] {s t : set α} {μ : measure α}
 
 /-- If for each `x : α`, exactly one of `g • x`, `g : G`, belongs to a measurable set `s`, then `s`
 is a fundamental domain for the action of `G` on `α`. -/
@@ -63,13 +64,23 @@ lemma mk' (h_meas : null_measurable_set s μ) (h_exists : ∀ x : α, ∃! g : G
   is_fundamental_domain G s μ :=
 { null_measurable_set := h_meas,
   ae_covers := eventually_of_forall $ λ x, (h_exists x).exists,
-  ae_disjoint := λ g hne, disjoint.ae_disjoint $ disjoint_left.2
+  ae_disjoint := λ a b hab, disjoint.ae_disjoint $ disjoint_left.2 $ λ x hxa hxb,
     begin
-      rintro _ ⟨x, hx, rfl⟩ hgx,
-      rw ← one_smul G x at hx,
-      exact hne ((h_exists x).unique hgx hx)
+      rw mem_smul_set_iff_inv_smul_mem at hxa hxb,
+      exact hab (inv_injective $ (h_exists x).unique hxa hxb),
     end }
 
+/-- For `s` to be a fundamental domain, it's enough to check `ae_disjoint (g • s) s` for `g ≠ 1`. -/
+@[to_additive "For `s` to be a fundamental domain, it's enough to check `ae_disjoint (g +ᵥ s) s` for
+`g ≠ 0`."]
+lemma mk'' (h_meas : null_measurable_set s μ) (h_ae_covers : ∀ᵐ x ∂μ, ∃ g : G, g • x ∈ s)
+  (h_ae_disjoint : ∀ g ≠ (1 : G), ae_disjoint μ (g • s) s)
+  (h_qmp : ∀ (g : G), quasi_measure_preserving ((•) g : α → α) μ μ) :
+  is_fundamental_domain G s μ :=
+{ null_measurable_set := h_meas,
+  ae_covers := h_ae_covers,
+  ae_disjoint := pairwise_ae_disjoint_of_ae_disjoint_forall_ne_one h_ae_disjoint h_qmp }
+
 /-- If a measurable space has a finite measure `μ` and a countable group `G` acts
 quasi-measure-preservingly, then to show that a set `s` is a fundamental domain, it is sufficient
 to check that its translates `g • s` are (almost) disjoint and that the sum `∑' g, μ (g • s)` is
@@ -85,12 +96,12 @@ lemma mk_of_measure_univ_le [is_finite_measure μ] [countable G]
   (h_qmp : ∀ (g : G), quasi_measure_preserving ((•) g : α → α) μ μ)
   (h_measure_univ_le : μ (univ : set α) ≤ ∑' (g : G), μ (g • s)) :
   is_fundamental_domain G s μ :=
+have ae_disjoint : pairwise (ae_disjoint μ on (λ (g : G), g • s)) :=
+  pairwise_ae_disjoint_of_ae_disjoint_forall_ne_one h_ae_disjoint h_qmp,
 { null_measurable_set := h_meas,
-  ae_disjoint := h_ae_disjoint,
+  ae_disjoint := ae_disjoint,
   ae_covers :=
   begin
-    replace ae_disjoint : pairwise (ae_disjoint μ on (λ (g : G), g • s)) :=
-      pairwise_ae_disjoint_of_ae_disjoint_forall_ne_one h_ae_disjoint h_qmp,
     replace h_meas : ∀ (g : G), null_measurable_set (g • s) μ :=
       λ g, by { rw [← inv_inv g, ← preimage_smul], exact h_meas.preimage (h_qmp g⁻¹), },
     have h_meas' : null_measurable_set {a | ∃ (g : G), g • a ∈ s} μ,
@@ -107,42 +118,20 @@ eventually_eq_univ.2 $ h.ae_covers.mono $ λ x ⟨g, hg⟩, mem_Union.2 ⟨g⁻
 
 @[to_additive] lemma mono (h : is_fundamental_domain G s μ) {ν : measure α} (hle : ν ≪ μ) :
   is_fundamental_domain G s ν :=
-⟨h.1.mono_ac hle, hle h.2, λ g hg, hle (h.3 g hg)⟩
-
-variables [measurable_space G] [has_measurable_smul G α] [smul_invariant_measure G α μ]
-
-@[to_additive] lemma null_measurable_set_smul (h : is_fundamental_domain G s μ) (g : G) :
-  null_measurable_set (g • s) μ :=
-h.null_measurable_set.smul g
-
-@[to_additive] lemma restrict_restrict (h : is_fundamental_domain G s μ) (g : G) (t : set α) :
-  (μ.restrict t).restrict (g • s) = μ.restrict (g • s ∩ t) :=
-restrict_restrict₀ ((h.null_measurable_set_smul g).mono restrict_le_self)
-
-@[to_additive] lemma pairwise_ae_disjoint (h : is_fundamental_domain G s μ) :
-  pairwise (λ g₁ g₂ : G, ae_disjoint μ (g₁ • s) (g₂ • s)) :=
-pairwise_ae_disjoint_of_ae_disjoint_forall_ne_one h.ae_disjoint
-  (λ g, measure_preserving.quasi_measure_preserving $ by simp)
-
-@[to_additive] lemma pairwise_ae_disjoint_of_ac {ν} (h : is_fundamental_domain G s μ) (hν : ν ≪ μ) :
-  pairwise (λ g₁ g₂ : G, ae_disjoint ν (g₁ • s) (g₂ • s)) :=
-h.pairwise_ae_disjoint.mono $ λ g₁ g₂ H, hν H
+⟨h.1.mono_ac hle, hle h.2, h.ae_disjoint.mono $ λ a b hab, hle hab⟩
 
 @[to_additive] lemma preimage_of_equiv {ν : measure β} (h : is_fundamental_domain G s μ) {f : β → α}
   (hf : quasi_measure_preserving f ν μ) {e : G → H} (he : bijective e)
   (hef : ∀ g, semiconj f ((•) (e g)) ((•) g)) :
   is_fundamental_domain H (f ⁻¹' s) ν :=
 { null_measurable_set := h.null_measurable_set.preimage hf,
   ae_covers := (hf.ae h.ae_covers).mono $ λ x ⟨g, hg⟩, ⟨e g, by rwa [mem_preimage, hef g x]⟩,
-  ae_disjoint := λ g hg,
+  ae_disjoint := λ a b hab,
     begin
       lift e to G ≃ H using he,
-      have : (e.symm g⁻¹)⁻¹ ≠ (e.symm 1)⁻¹, by simp [hg],
-      convert (h.pairwise_ae_disjoint this).preimage hf using 1,
-      { simp only [← preimage_smul_inv, preimage_preimage, ← hef _ _, e.apply_symm_apply,
-          inv_inv] },
-      { ext1 x,
-        simp only [mem_preimage, ← preimage_smul, ← hef _ _, e.apply_symm_apply, one_smul] }
+      have : (e.symm a⁻¹)⁻¹ ≠ (e.symm b⁻¹)⁻¹, by simp [hab],
+      convert (h.ae_disjoint this).preimage hf using 1,
+      simp only [←preimage_smul_inv, preimage_preimage, ←hef _ _, e.apply_symm_apply, inv_inv],
     end }
 
 @[to_additive] lemma image_of_equiv {ν : measure β} (h : is_fundamental_domain G s μ)
@@ -156,11 +145,9 @@ begin
   rw [← hef _ _, f.symm_apply_apply, f.symm_apply_apply, e.apply_symm_apply]
 end
 
-@[to_additive] lemma smul (h : is_fundamental_domain G s μ) (g : G) :
-  is_fundamental_domain G (g • s) μ :=
-h.image_of_equiv (mul_action.to_perm g) (measure_preserving_smul _ _).quasi_measure_preserving
-  ⟨λ g', g⁻¹ * g' * g, λ g', g * g' * g⁻¹, λ g', by simp [mul_assoc], λ g', by simp [mul_assoc]⟩ $
-  λ g' x, by simp [smul_smul, mul_assoc]
+@[to_additive] lemma pairwise_ae_disjoint_of_ac {ν} (h : is_fundamental_domain G s μ) (hν : ν ≪ μ) :
+  pairwise (λ g₁ g₂ : G, ae_disjoint ν (g₁ • s) (g₂ • s)) :=
+h.ae_disjoint.mono $ λ g₁ g₂ H, hν H
 
 @[to_additive] lemma smul_of_comm {G' : Type*} [group G'] [mul_action G' α] [measurable_space G']
   [has_measurable_smul G' α] [smul_invariant_measure G' α μ] [smul_comm_class G' G α]
@@ -169,11 +156,27 @@ h.image_of_equiv (mul_action.to_perm g) (measure_preserving_smul _ _).quasi_meas
 h.image_of_equiv (mul_action.to_perm g) (measure_preserving_smul _ _).quasi_measure_preserving
   (equiv.refl _) $ smul_comm g
 
+variables [measurable_space G] [has_measurable_smul G α] [smul_invariant_measure G α μ]
+
+@[to_additive] lemma null_measurable_set_smul (h : is_fundamental_domain G s μ) (g : G) :
+  null_measurable_set (g • s) μ :=
+h.null_measurable_set.smul g
+
+@[to_additive] lemma restrict_restrict (h : is_fundamental_domain G s μ) (g : G) (t : set α) :
+  (μ.restrict t).restrict (g • s) = μ.restrict (g • s ∩ t) :=
+restrict_restrict₀ ((h.null_measurable_set_smul g).mono restrict_le_self)
+
+@[to_additive] lemma smul (h : is_fundamental_domain G s μ) (g : G) :
+  is_fundamental_domain G (g • s) μ :=
+h.image_of_equiv (mul_action.to_perm g) (measure_preserving_smul _ _).quasi_measure_preserving
+  ⟨λ g', g⁻¹ * g' * g, λ g', g * g' * g⁻¹, λ g', by simp [mul_assoc], λ g', by simp [mul_assoc]⟩ $
+  λ g' x, by simp [smul_smul, mul_assoc]
+
 variables [countable G] {ν : measure α}
 
 @[to_additive] lemma sum_restrict_of_ac (h : is_fundamental_domain G s μ) (hν : ν ≪ μ) :
   sum (λ g : G, ν.restrict (g • s)) = ν :=
-by rw [← restrict_Union_ae (h.pairwise_ae_disjoint.mono $ λ i j h, hν h)
+by rw [← restrict_Union_ae (h.ae_disjoint.mono $ λ i j h, hν h)
     (λ g, (h.null_measurable_set_smul g).mono_ac hν),
   restrict_congr_set (hν h.Union_smul_ae_eq), restrict_univ]
 
@@ -338,7 +341,7 @@ begin
       by simp only [hf, hs.restrict_restrict]
     ... = ∫ x in ⋃ g : G, g • s, f x ∂(μ.restrict t) :
       (integral_Union_ae (λ g, (hs.null_measurable_set_smul g).mono_ac hac)
-        (hs.pairwise_ae_disjoint.mono $ λ i j h, hac h) hft.integrable.integrable_on).symm
+        (hs.ae_disjoint.mono $ λ i j h, hac h) hft.integrable.integrable_on).symm
     ... = ∫ x in t, f x ∂μ :
       by rw [restrict_congr_set (hac hs.Union_smul_ae_eq), restrict_univ] },
   { rw [integral_undef hfs, integral_undef],