refactor(measure_theory/group/basic): rename and split (#11952)

* Rename `measure_theory/group/basic` -> `measure_theory/group/measure`. It was not the bottom file in this folder in the import hierarchy (arithmetic is below it).
* Split off some results to `measure_theory/group/integration`. This reduces imports in some files, and makes the organization more clear. Furthermore, I will add some integrability results and more integrals in a follow-up PR.
* Prove a general instance `pi.is_mul_left_invariant`
* Remove lemmas specifically about `volume` on `real` in favor on the general lemmas.
```lean
real.map_volume_add_left -> map_add_left_eq_self
real.map_volume_pi_add_left -> map_add_left_eq_self
real.volume_preimage_add_left -> measure_preimage_add
real.volume_pi_preimage_add_left -> measure_preimage_add
real.map_volume_add_right -> map_add_right_eq_self 
real.volume_preimage_add_right -> measure_preimage_add_right
```

Author: fpvandoorn

src/analysis/box_integral/integrability.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import analysis.box_integral.basic
+import measure_theory.measure.regular
 
 /-!
 # McShane integrability vs Bochner integrability

src/analysis/fourier.lean

@@ -8,6 +8,7 @@ import analysis.inner_product_space.l2_space
 import measure_theory.function.continuous_map_dense
 import measure_theory.function.l2_space
 import measure_theory.measure.haar
+import measure_theory.group.integration
 import topology.metric_space.emetric_paracompact
 import topology.continuous_function.stone_weierstrass
 

src/measure_theory/constructions/pi.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
 import measure_theory.constructions.prod
+import measure_theory.group.measure
 
 /-!
 # Product measures
@@ -534,6 +535,18 @@ begin
   simp only [equiv.self_comp_symm, map_id]
 end
 
+@[to_additive] instance pi.is_mul_left_invariant [∀ i, group (α i)] [∀ i, has_measurable_mul (α i)]
+  [∀ i, is_mul_left_invariant (μ i)] : is_mul_left_invariant (measure.pi μ) :=
+begin
+  refine ⟨λ x, (measure.pi_eq (λ s hs, _)).symm⟩,
+  have A : has_mul.mul x ⁻¹' (set.pi univ (λ (i : ι), s i))
+    = set.pi univ (λ (i : ι), ((*) (x i)) ⁻¹' (s i)), by { ext, simp },
+  rw [measure.map_apply (measurable_const_mul x) (measurable_set.univ_pi_fintype hs), A,
+      pi_pi],
+  simp only [measure_preimage_mul]
+end
+
+
 end measure
 instance measure_space.pi [Π i, measure_space (α i)] : measure_space (Π i, α i) :=
 ⟨measure.pi (λ i, volume)⟩
@@ -557,6 +570,14 @@ lemma volume_pi_closed_ball [Π i, measure_space (α i)] [∀ i, sigma_finite (v
   volume (metric.closed_ball x r) = ∏ i, volume (metric.closed_ball (x i) r) :=
 measure.pi_closed_ball _ _ hr
 
+open measure
+@[to_additive]
+instance pi.is_mul_left_invariant_volume [∀ i, group (α i)] [Π i, measure_space (α i)]
+  [∀ i, sigma_finite (volume : measure (α i))]
+  [∀ i, has_measurable_mul (α i)] [∀ i, is_mul_left_invariant (volume : measure (α i))] :
+  is_mul_left_invariant (volume : measure (Π i, α i)) :=
+pi.is_mul_left_invariant _
+
 /-!
 ### Measure preserving equivalences
 

src/measure_theory/group/arithmetic.lean

@@ -131,6 +131,13 @@ measurable_mul.comp_ae_measurable (hf.prod_mk hg)
 
 omit m
 
+@[to_additive]
+instance pi.has_measurable_mul {ι : Type*} {α : ι → Type*} [∀ i, has_mul (α i)]
+  [∀ i, measurable_space (α i)] [∀ i, has_measurable_mul (α i)] :
+  has_measurable_mul (Π i, α i) :=
+⟨λ g, measurable_pi_iff.mpr $ λ i, (measurable_const_mul (g i)).comp $ measurable_pi_apply i,
+ λ g, measurable_pi_iff.mpr $ λ i, (measurable_mul_const (g i)).comp $ measurable_pi_apply i⟩
+
 @[priority 100, to_additive]
 instance has_measurable_mul₂.to_has_measurable_mul [has_measurable_mul₂ M] :
   has_measurable_mul M :=

src/measure_theory/group/integration.lean

@@ -0,0 +1,108 @@
+/-
+Copyright (c) 2022 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+-/
+import measure_theory.integral.bochner
+import measure_theory.group.measure
+
+/-!
+# Integration on Groups
+
+We develop properties of integrals with a group as domain.
+This file contains properties about integrability, Lebesgue integration and Bochner integration.
+-/
+
+namespace measure_theory
+
+open measure topological_space
+open_locale ennreal
+
+variables {𝕜 G E : Type*} [measurable_space G] {μ : measure G}
+variables [normed_group E] [second_countable_topology E] [normed_space ℝ E] [complete_space E]
+  [measurable_space E] [borel_space E]
+
+section measurable_mul
+
+variables [group G] [has_measurable_mul G]
+
+/-- Translating a function by left-multiplication does not change its `lintegral` with respect to
+a left-invariant measure. -/
+@[to_additive]
+lemma lintegral_mul_left_eq_self [is_mul_left_invariant μ] (f : G → ℝ≥0∞) (g : G) :
+  ∫⁻ x, f (g * x) ∂μ = ∫⁻ x, f x ∂μ :=
+begin
+  convert (lintegral_map_equiv f $ measurable_equiv.mul_left g).symm,
+  simp [map_mul_left_eq_self μ g]
+end
+
+/-- Translating a function by right-multiplication does not change its `lintegral` with respect to
+a right-invariant measure. -/
+@[to_additive]
+lemma lintegral_mul_right_eq_self [is_mul_right_invariant μ] (f : G → ℝ≥0∞) (g : G) :
+  ∫⁻ x, f (x * g) ∂μ = ∫⁻ x, f x ∂μ :=
+begin
+  convert (lintegral_map_equiv f $ measurable_equiv.mul_right g).symm,
+  simp [map_mul_right_eq_self μ g]
+end
+
+/-- Translating a function by left-multiplication does not change its integral with respect to a
+left-invariant measure. -/
+@[to_additive]
+lemma integral_mul_left_eq_self [is_mul_left_invariant μ] (f : G → E) (g : G) :
+  ∫ x, f (g * x) ∂μ = ∫ x, f x ∂μ :=
+begin
+  have h_mul : measurable_embedding (λ x, g * x) :=
+    (measurable_equiv.mul_left g).measurable_embedding,
+  rw [← h_mul.integral_map, map_mul_left_eq_self]
+end
+
+/-- Translating a function by right-multiplication does not change its integral with respect to a
+right-invariant measure. -/
+@[to_additive]
+lemma integral_mul_right_eq_self [is_mul_right_invariant μ] (f : G → E) (g : G) :
+  ∫ x, f (x * g) ∂μ = ∫ x, f x ∂μ :=
+begin
+  have h_mul : measurable_embedding (λ x, x * g) :=
+    (measurable_equiv.mul_right g).measurable_embedding,
+  rw [← h_mul.integral_map, map_mul_right_eq_self]
+end
+
+/-- If some left-translate of a function negates it, then the integral of the function with respect
+to a left-invariant measure is 0. -/
+@[to_additive]
+lemma integral_zero_of_mul_left_eq_neg [is_mul_left_invariant μ] {f : G → E} {g : G}
+  (hf' : ∀ x, f (g * x) = - f x) :
+  ∫ x, f x ∂μ = 0 :=
+by simp_rw [← self_eq_neg ℝ E, ← integral_neg, ← hf', integral_mul_left_eq_self]
+
+/-- If some right-translate of a function negates it, then the integral of the function with respect
+to a right-invariant measure is 0. -/
+@[to_additive]
+lemma integral_zero_of_mul_right_eq_neg [is_mul_right_invariant μ] {f : G → E} {g : G}
+  (hf' : ∀ x, f (x * g) = - f x) :
+  ∫ x, f x ∂μ = 0 :=
+by simp_rw [← self_eq_neg ℝ E, ← integral_neg, ← hf', integral_mul_right_eq_self]
+
+end measurable_mul
+
+
+section topological_group
+
+variables [topological_space G] [group G] [topological_group G] [borel_space G]
+  [is_mul_left_invariant μ]
+
+/-- For nonzero regular left invariant measures, the integral of a continuous nonnegative function
+  `f` is 0 iff `f` is 0. -/
+@[to_additive]
+lemma lintegral_eq_zero_of_is_mul_left_invariant [regular μ] (hμ : μ ≠ 0)
+  {f : G → ℝ≥0∞} (hf : continuous f) :
+  ∫⁻ x, f x ∂μ = 0 ↔ f = 0 :=
+begin
+  haveI := is_open_pos_measure_of_mul_left_invariant_of_regular hμ,
+  rw [lintegral_eq_zero_iff hf.measurable, hf.ae_eq_iff_eq μ continuous_zero]
+end
+
+end topological_group
+
+end measure_theory

src/measure_theory/group/basic.lean renamed to src/measure_theory/group/measure.lean

@@ -3,7 +3,6 @@ Copyright (c) 2020 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
-import measure_theory.integral.lebesgue
 import measure_theory.measure.regular
 import measure_theory.group.measurable_equiv
 import measure_theory.measure.open_pos
@@ -13,7 +12,7 @@ import measure_theory.measure.open_pos
 
 We develop some properties of measures on (topological) groups
 
-* We define properties on measures: left and right invariant measures.
+* We define properties on measures: measures that are left or right invariant w.r.t. multiplication.
 * We define the measure `μ.inv : A ↦ μ(A⁻¹)` and show that it is right invariant iff
   `μ` is left invariant.
 * We define a class `is_haar_measure μ`, requiring that the measure `μ` is left-invariant, finite
@@ -259,17 +258,6 @@ lemma measure_lt_top_of_is_compact_of_is_mul_left_invariant'
 measure_lt_top_of_is_compact_of_is_mul_left_invariant (interior U) is_open_interior hU
   ((measure_mono (interior_subset)).trans_lt (lt_top_iff_ne_top.2 h)).ne hK
 
-/-- For nonzero regular left invariant measures, the integral of a continuous nonnegative function
-  `f` is 0 iff `f` is 0. -/
-@[to_additive]
-lemma lintegral_eq_zero_of_is_mul_left_invariant [regular μ] (hμ : μ ≠ 0)
-  {f : G → ℝ≥0∞} (hf : continuous f) :
-  ∫⁻ x, f x ∂μ = 0 ↔ f = 0 :=
-begin
-  haveI := is_open_pos_measure_of_mul_left_invariant_of_regular hμ,
-  rw [lintegral_eq_zero_iff hf.measurable, hf.ae_eq_iff_eq μ continuous_zero]
-end
-
 end group
 
 section comm_group
@@ -287,32 +275,6 @@ instance is_mul_left_invariant.is_mul_right_invariant {μ : measure G} [is_mul_l
 
 end comm_group
 
-section integration
-
-variables [group G] [has_measurable_mul G] {μ : measure G}
-
-/-- Translating a function by left-multiplication does not change its `lintegral` with respect to
-a left-invariant measure. -/
-@[to_additive]
-lemma lintegral_mul_left_eq_self [is_mul_left_invariant μ] (f : G → ℝ≥0∞) (g : G) :
-  ∫⁻ x, f (g * x) ∂μ = ∫⁻ x, f x ∂μ :=
-begin
-  convert (lintegral_map_equiv f $ measurable_equiv.mul_left g).symm,
-  simp [map_mul_left_eq_self μ g]
-end
-
-/-- Translating a function by right-multiplication does not change its `lintegral` with respect to
-a right-invariant measure. -/
-@[to_additive]
-lemma lintegral_mul_right_eq_self [is_mul_right_invariant μ] (f : G → ℝ≥0∞) (g : G) :
-  ∫⁻ x, f (x * g) ∂μ = ∫⁻ x, f x ∂μ :=
-begin
-  convert (lintegral_map_equiv f $ measurable_equiv.mul_right g).symm,
-  simp [map_mul_right_eq_self μ g]
-end
-
-end integration
-
 section haar
 
 namespace measure

src/measure_theory/group/prod.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
 import measure_theory.constructions.prod
+import measure_theory.group.measure
 
 /-!
 # Measure theory in the product of groups

src/measure_theory/integral/bochner.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Zhouhang Zhou, Yury Kudryashov, Sébastien Gouëzel, Rémy Degenne
 -/
 import measure_theory.integral.set_to_l1
-import measure_theory.group.basic
 import analysis.normed_space.bounded_linear_maps
 import topology.sequences
 
@@ -1296,53 +1295,6 @@ calc ∫ x, f x ∂(measure.dirac a) = ∫ x, f a ∂(measure.dirac a) :
 
 end properties
 
-section group
-
-variables {G : Type*} [measurable_space G] [group G] [has_measurable_mul G]
-variables {μ : measure G}
-
-open measure
-
-/-- Translating a function by left-multiplication does not change its integral with respect to a
-left-invariant measure. -/
-@[to_additive]
-lemma integral_mul_left_eq_self [is_mul_left_invariant μ] (f : G → E) (g : G) :
-  ∫ x, f (g * x) ∂μ = ∫ x, f x ∂μ :=
-begin
-  have h_mul : measurable_embedding (λ x, g * x) :=
-    (measurable_equiv.mul_left g).measurable_embedding,
-  rw [← h_mul.integral_map, map_mul_left_eq_self]
-end
-
-/-- Translating a function by right-multiplication does not change its integral with respect to a
-right-invariant measure. -/
-@[to_additive]
-lemma integral_mul_right_eq_self [is_mul_right_invariant μ] (f : G → E) (g : G) :
-  ∫ x, f (x * g) ∂μ = ∫ x, f x ∂μ :=
-begin
-  have h_mul : measurable_embedding (λ x, x * g) :=
-    (measurable_equiv.mul_right g).measurable_embedding,
-  rw [← h_mul.integral_map, map_mul_right_eq_self]
-end
-
-/-- If some left-translate of a function negates it, then the integral of the function with respect
-to a left-invariant measure is 0. -/
-@[to_additive]
-lemma integral_zero_of_mul_left_eq_neg [is_mul_left_invariant μ] {f : G → E} {g : G}
-  (hf' : ∀ x, f (g * x) = - f x) :
-  ∫ x, f x ∂μ = 0 :=
-by simp_rw [← self_eq_neg ℝ E, ← integral_neg, ← hf', integral_mul_left_eq_self]
-
-/-- If some right-translate of a function negates it, then the integral of the function with respect
-to a right-invariant measure is 0. -/
-@[to_additive]
-lemma integral_zero_of_mul_right_eq_neg [is_mul_right_invariant μ] {f : G → E} {g : G}
-  (hf' : ∀ x, f (x * g) = - f x) :
-  ∫ x, f x ∂μ = 0 :=
-by simp_rw [← self_eq_neg ℝ E, ← integral_neg, ← hf', integral_mul_right_eq_self]
-
-end group
-
 mk_simp_attribute integral_simps "Simp set for integral rules."
 
 attribute [integral_simps] integral_neg integral_smul L1.integral_add L1.integral_sub

src/measure_theory/integral/interval_integral.lean

@@ -666,7 +666,7 @@ have A : measurable_embedding (λ x, x + d) :=
 calc  ∫ x in a..b, f (x + d)
     = ∫ x in a+d..b+d, f x ∂(measure.map (λ x, x + d) volume)
                            : by simp [interval_integral, A.set_integral_map]
-... = ∫ x in a+d..b+d, f x : by rw [real.map_volume_add_right]
+... = ∫ x in a+d..b+d, f x : by rw [map_add_right_eq_self]
 
 @[simp] lemma integral_comp_add_left (d) :
   ∫ x in a..b, f (d + x) = ∫ x in d+a..d+b, f x :=

src/measure_theory/integral/periodic.lean

@@ -40,11 +40,11 @@ begin
   haveI : encodable (add_subgroup.zmultiples a) := (countable_range _).to_encodable,
   simp only [interval_integral.integral_of_le, ha.le, le_add_iff_nonneg_right],
   haveI : vadd_invariant_measure (add_subgroup.zmultiples a) ℝ volume :=
-    ⟨λ c s hs, real.volume_preimage_add_left _ _⟩,
+    ⟨λ c s hs, measure_preimage_add _ _ _⟩,
   exact (is_add_fundamental_domain_Ioc ha b).set_integral_eq
     (is_add_fundamental_domain_Ioc ha c) hf.map_vadd_zmultiples
 end
-  
+
 /-- If `f` is a periodic function with period `a`, then its integral over `[b, b + a]` does not
 depend on `b`. -/
 lemma interval_integral_add_eq {f : ℝ → E} {a : ℝ} (hf : periodic f a)