feat(measure_theory/group/fundamental_domain): prove equality of inte…

…grals (#10448)

src/dynamics/ergodic/measure_preserving.lean

@@ -70,6 +70,11 @@ lemma restrict_image_emb {f : α → β} (hf : measure_preserving f μa μb) (h
   (s : set α) : measure_preserving f (μa.restrict s) (μb.restrict (f '' s)) :=
 by simpa only [preimage_image_eq _ h₂.injective] using hf.restrict_preimage_emb h₂ (f '' s)
 
+lemma ae_measurable_comp_iff {f : α → β} (hf : measure_preserving f μa μb)
+  (h₂ : measurable_embedding f) {g : β → γ} :
+  ae_measurable (g ∘ f) μa ↔ ae_measurable g μb :=
+by rw [← hf.map_eq, h₂.ae_measurable_map_iff]
+
 protected lemma quasi_measure_preserving {f : α → β} (hf : measure_preserving f μa μb) :
   quasi_measure_preserving f μa μb :=
 ⟨hf.1, hf.2.absolutely_continuous⟩

src/measure_theory/group/fundamental_domain.lean

@@ -5,6 +5,7 @@ Authors: Yury G. Kudryashov
 -/
 import measure_theory.group.action
 import measure_theory.group.pointwise
+import measure_theory.integral.set_integral
 
 /-!
 # Fundamental domain of a group action
@@ -20,13 +21,14 @@ with respect to a measure `μ` if
   we require this for `g₂ = 1` in the definition, then deduce it for any two `g₁ ≠ g₂`.
 
 In this file we prove that in case of a countable group `G` and a measure preserving action, any two
-fundamental domains have the same measure.
+fundamental domains have the same measure, and for a `G`-invariant function, its integrals over any
+two fundamental domains are equal to each other.
 
 We also generate additive versions of all theorems in this file using the `to_additive` attribute.
 -/
 
-open_locale ennreal pointwise topological_space nnreal ennreal
-open measure_theory measure_theory.measure set function
+open_locale ennreal pointwise topological_space nnreal ennreal measure_theory
+open measure_theory measure_theory.measure set function topological_space
 
 namespace measure_theory
 
@@ -51,14 +53,18 @@ structure is_fundamental_domain (G : Type*) {α : Type*} [has_one G] [has_scalar
 
 namespace is_fundamental_domain
 
-variables {G α : Type*} [group G] [mul_action G α] [measurable_space α] {s t : set α}
-  {μ : measure α}
+variables {G α E : Type*} [group G] [mul_action G α] [measurable_space α]
+  [normed_group E] {s t : set α} {μ : measure α}
 
 @[to_additive] lemma Union_smul_ae_eq (h : is_fundamental_domain G s μ) :
   (⋃ g : G, g • s) =ᵐ[μ] univ :=
 filter.eventually_eq_univ.2 $ h.ae_covers.mono $
   λ x ⟨g, hg⟩, mem_Union.2 ⟨g⁻¹, _, hg, inv_smul_smul _ _⟩
 
+@[to_additive] lemma mono (h : is_fundamental_domain G s μ) {ν : measure α} (hle : ν ≪ μ) :
+  is_fundamental_domain G s ν :=
+⟨h.1, hle h.2, λ g hg, hle (h.3 g hg)⟩
+
 variables [measurable_space G] [has_measurable_smul G α]
 
 @[to_additive]
@@ -75,31 +81,138 @@ calc μ (g₁ • s ∩ g₂ • s) = μ (g₂ • ((g₂⁻¹ * g₁) • s ∩
 ... = μ ((g₂⁻¹ * g₁) • s ∩ s) : measure_smul_set _ _ _
 ... = 0 : h.ae_disjoint _ $ mt inv_mul_eq_one.1 hne.symm
 
-variables [encodable G]
+variables [encodable 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) h.measurable_set_smul,
+  restrict_congr_set (hν h.Union_smul_ae_eq), restrict_univ]
+
+@[to_additive] lemma lintegral_eq_tsum_of_ac (h : is_fundamental_domain G s μ) (hν : ν ≪ μ)
+  (f : α → ℝ≥0∞) : ∫⁻ x, f x ∂ν = ∑' g : G, ∫⁻ x in g • s, f x ∂ν :=
+by rw [← lintegral_sum_measure, h.sum_restrict_of_ac hν]
+
+@[to_additive] lemma set_lintegral_eq_tsum' (h : is_fundamental_domain G s μ) (f : α → ℝ≥0∞)
+  (t : set α) : ∫⁻ x in t, f x ∂μ = ∑' g : G, ∫⁻ x in t ∩ g • s, f x ∂μ :=
+calc ∫⁻ x in t, f x ∂μ = ∑' g : G, ∫⁻ x in g • s, f x ∂(μ.restrict t) :
+  h.lintegral_eq_tsum_of_ac restrict_le_self.absolutely_continuous _
+... = ∑' g : G, ∫⁻ x in t ∩ g • s, f x ∂μ :
+  by simp only [restrict_restrict, h.measurable_set_smul, inter_comm]
+
+@[to_additive] lemma set_lintegral_eq_tsum (h : is_fundamental_domain G s μ) (f : α → ℝ≥0∞)
+  (t : set α) :
+  ∫⁻ x in t, f x ∂μ = ∑' g : G, ∫⁻ x in g • t ∩ s, f (g⁻¹ • x) ∂μ :=
+calc ∫⁻ x in t, f x ∂μ = ∑' g : G, ∫⁻ x in t ∩ g • s, f x ∂μ :
+  h.set_lintegral_eq_tsum' f t
+... = ∑' g : G, ∫⁻ x in t ∩ g⁻¹ • s, f x ∂μ : ((equiv.inv G).tsum_eq _).symm
+... = ∑' g : G, ∫⁻ x in g⁻¹ • (g • t ∩ s), f (x) ∂μ :
+  by simp only [smul_set_inter, inv_smul_smul]
+... = ∑' g : G, ∫⁻ x in g • t ∩ s, f (g⁻¹ • x) ∂μ :
+  tsum_congr $ λ g, ((measure_preserving_smul g⁻¹ μ).set_lintegral_comp_emb
+    (measurable_embedding_const_smul _) _ _).symm
+
+@[to_additive] lemma measure_eq_tsum_of_ac (h : is_fundamental_domain G s μ) (hν : ν ≪ μ)
+  (t : set α) :
+  ν t = ∑' g : G, ν (t ∩ g • s) :=
+by simpa only [set_lintegral_one, pi.one_def, measure.restrict_apply (h.measurable_set_smul _),
+  inter_comm]
+  using h.lintegral_eq_tsum_of_ac (measure.restrict_le_self.absolutely_continuous.trans hν) 1
 
 @[to_additive] lemma measure_eq_tsum' (h : is_fundamental_domain G s μ) (t : set α) :
   μ t = ∑' g : G, μ (t ∩ g • s) :=
-calc μ t = μ.restrict t (⋃ g : G, g • s) :
-  by rw [measure_congr (ae_mono measure.restrict_le_self h.Union_smul_ae_eq), restrict_apply_univ]
-... = ∑' g : G, μ.restrict t (g • s) :
-  measure_Union_of_null_inter h.measurable_set_smul $ h.pairwise_ae_disjoint.mono $
-    λ g₁ g₂ H, measure.restrict_le_self.absolutely_continuous H
-... = ∑' g : G, μ (t ∩ g • s) :
-  tsum_congr $ λ g, by rw [measure.restrict_apply (h.measurable_set_smul g), inter_comm]
+h.measure_eq_tsum_of_ac absolutely_continuous.rfl t
 
 @[to_additive] lemma measure_eq_tsum (h : is_fundamental_domain G s μ) (t : set α) :
   μ t = ∑' g : G, μ (g • t ∩ s) :=
-calc μ t = ∑' g : G, μ (t ∩ g • s) : h.measure_eq_tsum' t
-     ... = ∑' g : G, μ (t ∩ g⁻¹ • s) : ((equiv.inv G).tsum_eq _).symm
-     ... = ∑' g : G, μ (g • t ∩ s) :
-  tsum_congr $ λ g, by rw [← measure_smul_set g μ, smul_set_inter, smul_inv_smul]
+by simpa only [set_lintegral_one] using h.set_lintegral_eq_tsum (λ _, 1) t
+
+@[to_additive] protected lemma set_lintegral_eq (hs : is_fundamental_domain G s μ)
+  (ht : is_fundamental_domain G t μ) (f : α → ℝ≥0∞) (hf : ∀ (g : G) x, f (g • x) = f x) :
+  ∫⁻ x in s, f x ∂μ = ∫⁻ x in t, f x ∂μ :=
+calc ∫⁻ x in s, f x ∂μ = ∑' g : G, ∫⁻ x in s ∩ g • t, f x ∂μ :
+  ht.set_lintegral_eq_tsum' _ _
+... = ∑' g : G, ∫⁻ x in g • t ∩ s, f (g⁻¹ • x) ∂μ :
+  by simp only [hf, inter_comm]
+... = ∫⁻ x in t, f x ∂μ :
+  (hs.set_lintegral_eq_tsum _ _).symm
 
 /-- 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 :=
-calc μ s = ∑' g : G, μ (s ∩ g • t) : ht.measure_eq_tsum' s
-     ... = ∑' g : G, μ (g • t ∩ s) : by simp only [inter_comm]
-     ... = μ t : (hs.measure_eq_tsum t).symm
+by simpa only [set_lintegral_one] using hs.set_lintegral_eq ht (λ _, 1) (λ _ _, rfl)
+
+@[to_additive] protected lemma ae_measurable_on_iff {β : Type*} [measurable_space β]
+  (hs : is_fundamental_domain G s μ) (ht : is_fundamental_domain G t μ) {f : α → β}
+  (hf : ∀ (g : G) x, f (g • x) = f x) :
+  ae_measurable f (μ.restrict s) ↔ ae_measurable f (μ.restrict t) :=
+calc ae_measurable f (μ.restrict s)
+    ↔ ae_measurable f (measure.sum $ λ g : G, (μ.restrict (g • t ∩ s))) :
+  by simp only [← restrict_restrict (ht.measurable_set_smul _),
+    ht.sum_restrict_of_ac restrict_le_self.absolutely_continuous]
+... ↔ ∀ g : G, ae_measurable f (μ.restrict (g • (g⁻¹ • s ∩ t))) :
+  by simp only [smul_set_inter, inter_comm, smul_inv_smul, ae_measurable_sum_measure_iff]
+... ↔ ∀ g : G, ae_measurable f (μ.restrict (g⁻¹ • (g⁻¹⁻¹ • s ∩ t))) : inv_surjective.forall
+... ↔ ∀ g : G, ae_measurable f (μ.restrict (g⁻¹ • (g • s ∩ t))) : by simp only [inv_inv]
+... ↔ ∀ g : G, ae_measurable f (μ.restrict (g • s ∩ t)) :
+  begin
+    refine forall_congr (λ g, _),
+    have he : measurable_embedding ((•) g⁻¹ : α → α) := measurable_embedding_const_smul _,
+    rw [← image_smul,
+      ← ((measure_preserving_smul g⁻¹ μ).restrict_image_emb he _).ae_measurable_comp_iff he],
+    simp only [(∘), hf]
+  end
+... ↔ ae_measurable f (μ.restrict t) :
+  by simp only [← ae_measurable_sum_measure_iff, ← restrict_restrict (hs.measurable_set_smul _),
+    hs.sum_restrict_of_ac restrict_le_self.absolutely_continuous]
+
+@[to_additive] protected lemma has_finite_integral_on_iff (hs : is_fundamental_domain G s μ)
+  (ht : is_fundamental_domain G t μ) {f : α → E} (hf : ∀ (g : G) x, f (g • x) = f x) :
+  has_finite_integral f (μ.restrict s) ↔ has_finite_integral f (μ.restrict t) :=
+begin
+  dunfold has_finite_integral,
+  rw hs.set_lintegral_eq ht,
+  intros g x, rw hf
+end
+
+variables [measurable_space E]
+
+@[to_additive] protected lemma integrable_on_iff (hs : is_fundamental_domain G s μ)
+  (ht : is_fundamental_domain G t μ) {f : α → E} (hf : ∀ (g : G) x, f (g • x) = f x) :
+  integrable_on f s μ ↔ integrable_on f t μ :=
+and_congr (hs.ae_measurable_on_iff ht hf) (hs.has_finite_integral_on_iff ht hf)
+
+variables [normed_space ℝ E] [borel_space E] [complete_space E] [second_countable_topology E]
+
+@[to_additive] protected lemma set_integral_eq (hs : is_fundamental_domain G s μ)
+  (ht : is_fundamental_domain G t μ) {f : α → E} (hf : ∀ (g : G) x, f (g • x) = f x) :
+  ∫ x in s, f x ∂μ = ∫ x in t, f x ∂μ :=
+begin
+  by_cases hfs : integrable_on f s μ,
+  { have hft : integrable_on f t μ, by rwa ht.integrable_on_iff hs hf,
+    have hac : ∀ {u}, μ.restrict u ≪ μ := λ u, restrict_le_self.absolutely_continuous,
+    calc ∫ x in s, f x ∂μ = ∫ x in ⋃ g : G, g • t, f x ∂(μ.restrict s) :
+      by rw [restrict_congr_set (hac ht.Union_smul_ae_eq), restrict_univ]
+    ... = ∑' g : G, ∫ x in g • t, f x ∂(μ.restrict s) :
+      integral_Union_of_null_inter ht.measurable_set_smul
+        (ht.pairwise_ae_disjoint.mono $ λ i j h, hac h) hfs.integrable.integrable_on
+    ... = ∑' g : G, ∫ x in s ∩ g • t, f x ∂μ :
+      by simp only [restrict_restrict (ht.measurable_set_smul _), inter_comm]
+    ... = ∑' g : G, ∫ x in s ∩ g⁻¹ • t, f x ∂μ : ((equiv.inv G).tsum_eq _).symm
+    ... = ∑' g : G, ∫ x in g⁻¹ • (g • s ∩ t), f x ∂μ :
+      by simp only [smul_set_inter, inv_smul_smul]
+    ... = ∑' g : G, ∫ x in g • s ∩ t, f (g⁻¹ • x) ∂μ :
+      tsum_congr $ λ g, (measure_preserving_smul g⁻¹ μ).set_integral_image_emb
+        (measurable_embedding_const_smul _) _ _
+    ... = ∑' g : G, ∫ x in g • s, f x ∂(μ.restrict t) :
+      by simp only [hf, restrict_restrict (hs.measurable_set_smul _)]
+    ... = ∫ x in ⋃ g : G, g • s, f x ∂(μ.restrict t) :
+      (integral_Union_of_null_inter hs.measurable_set_smul
+        (hs.pairwise_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],
+    rwa [hs.integrable_on_iff ht hf] at hfs }
+end
 
 end is_fundamental_domain