feat(measure_theory/group/prod): add properties for right-invariant m…

…easures (#16913)

* Use `measure_preserving` more in `measure_theory.group.measure`.
* Add instance `is_haar_measure.is_inv_invariant` for abelian groups; remove two (unused) lemmas that are a consequence of this.
* Improve docstrings in `measure_theory.group.prod`
* Sort the file `measure_theory.group.prod` now in sections `left_invariant`, `right_invariant`, `quasi_measure_preserving`
* Continuation of #16668
* Part of #16706

src/analysis/convolution.lean

@@ -223,7 +223,8 @@ variables [sigma_finite μ] [is_add_right_invariant μ]
 lemma measure_theory.ae_strongly_measurable.convolution_integrand
   (hf : ae_strongly_measurable f μ) (hg : ae_strongly_measurable g μ) :
   ae_strongly_measurable (λ p : G × G, L (f p.2) (g (p.1 - p.2))) (μ.prod μ) :=
-hf.convolution_integrand' L $ hg.mono' (quasi_measure_preserving_sub μ).absolutely_continuous
+hf.convolution_integrand' L $ hg.mono'
+  (quasi_measure_preserving_sub_of_right_invariant μ μ).absolutely_continuous
 
 lemma measure_theory.integrable.convolution_integrand (hf : integrable f μ) (hg : integrable g μ) :
   integrable (λ p : G × G, L (f p.2) (g (p.1 - p.2))) (μ.prod μ) :=

src/measure_theory/constructions/prod.lean

@@ -89,7 +89,7 @@ end
 
 variables [measurable_space α] [measurable_space α'] [measurable_space β] [measurable_space β']
 variables [measurable_space γ]
-variables {μ : measure α} {ν : measure β} {τ : measure γ}
+variables {μ μ' : measure α} {ν ν' : measure β} {τ : measure γ}
 variables [normed_add_comm_group E]
 
 /-! ### Measurability
@@ -325,7 +325,7 @@ bind μ $ λ x : α, map (prod.mk x) ν
 instance prod.measure_space {α β} [measure_space α] [measure_space β] : measure_space (α × β) :=
 { volume := volume.prod volume }
 
-variables {μ ν} [sigma_finite ν]
+variables [sigma_finite ν]
 
 lemma volume_eq_prod (α β) [measure_space α] [measure_space β] :
   (volume : measure (α × β)) = (volume : measure α).prod (volume : measure β) :=
@@ -449,6 +449,14 @@ begin
     eventually_of_forall $ λ x, zero_le _⟩
 end
 
+lemma absolutely_continuous.prod [sigma_finite ν'] (h1 : μ ≪ μ') (h2 : ν ≪ ν') :
+  μ.prod ν ≪ μ'.prod ν' :=
+begin
+  refine absolutely_continuous.mk (λ s hs h2s, _),
+  simp_rw [measure_prod_null hs] at h2s ⊢,
+  exact (h2s.filter_mono h1.ae_le).mono (λ _ h, h2 h)
+end
+
 /-- Note: the converse is not true. For a counterexample, see
   Walter Rudin *Real and Complex Analysis*, example (c) in section 8.9. -/
 lemma ae_ae_of_ae_prod {p : α × β → Prop} (h : ∀ᵐ z ∂μ.prod ν, p z) :

src/measure_theory/group/integration.lean

@@ -140,15 +140,7 @@ variables [has_measurable_inv G]
 lemma integrable.comp_div_left {f : G → F}
   [is_inv_invariant μ] [is_mul_left_invariant μ] (hf : integrable f μ) (g : G) :
   integrable (λ t, f (g / t)) μ :=
-begin
-  rw [← map_mul_right_inv_eq_self μ g⁻¹, integrable_map_measure, function.comp],
-  { simp_rw [div_inv_eq_mul, mul_inv_cancel_left], exact hf },
-  { refine ae_strongly_measurable.comp_measurable _ (measurable_id.const_div g),
-    simp_rw [map_map (measurable_id'.const_div g) (measurable_id'.const_mul g⁻¹).inv,
-      function.comp, div_inv_eq_mul, mul_inv_cancel_left, map_id'],
-    exact hf.ae_strongly_measurable },
-  { exact (measurable_id'.const_mul g⁻¹).inv.ae_measurable }
-end
+((measure_preserving_div_left μ g).integrable_comp hf.ae_strongly_measurable).mpr hf
 
 @[simp, to_additive]
 lemma integrable_comp_div_left (f : G → F)
@@ -183,7 +175,6 @@ end
 
 end smul
 
-
 section topological_group
 
 variables [topological_space G] [group G] [topological_group G] [borel_space G]

src/measure_theory/group/measure.lean

@@ -229,6 +229,13 @@ is_inv_invariant.inv_eq_self
 lemma map_inv_eq_self (μ : measure G) [is_inv_invariant μ] : map has_inv.inv μ = μ :=
 is_inv_invariant.inv_eq_self
 
+variables [has_measurable_inv G]
+
+@[to_additive]
+lemma measure_preserving_inv (μ : measure G) [is_inv_invariant μ] :
+  measure_preserving has_inv.inv μ μ :=
+⟨measurable_inv, map_inv_eq_self μ⟩
+
 end inv
 
 section has_involutive_inv
@@ -282,21 +289,28 @@ begin
 end
 
 @[to_additive]
-lemma map_div_left_eq_self (μ : measure G) [is_inv_invariant μ] [is_mul_left_invariant μ] (g : G) :
-  map (λ t, g / t) μ = μ :=
+lemma measure_preserving_div_left (μ : measure G) [is_inv_invariant μ] [is_mul_left_invariant μ]
+  (g : G) : measure_preserving (λ t, g / t) μ μ :=
 begin
   simp_rw [div_eq_mul_inv],
-  conv_rhs { rw [← map_mul_left_eq_self μ g, ← map_inv_eq_self μ] },
-  exact (map_map (measurable_const_mul g) measurable_inv).symm
+  exact (measure_preserving_mul_left μ g).comp (measure_preserving_inv μ)
 end
 
+@[to_additive]
+lemma map_div_left_eq_self (μ : measure G) [is_inv_invariant μ] [is_mul_left_invariant μ] (g : G) :
+  map (λ t, g / t) μ = μ :=
+(measure_preserving_div_left μ g).map_eq
+
+@[to_additive]
+lemma measure_preserving_mul_right_inv (μ : measure G)
+  [is_inv_invariant μ] [is_mul_left_invariant μ] (g : G) :
+  measure_preserving (λ t, (g * t)⁻¹) μ μ :=
+(measure_preserving_inv μ).comp $ measure_preserving_mul_left μ g
+
 @[to_additive]
 lemma map_mul_right_inv_eq_self (μ : measure G) [is_inv_invariant μ] [is_mul_left_invariant μ]
   (g : G) : map (λ t, (g * t)⁻¹) μ = μ :=
-begin
-  conv_rhs { rw [← map_inv_eq_self μ, ← map_mul_left_eq_self μ g] },
-  exact (map_map measurable_inv (measurable_const_mul g)).symm
-end
+(measure_preserving_mul_right_inv μ g).map_eq
 
 @[to_additive]
 lemma map_div_left_ae (μ : measure G) [is_mul_left_invariant μ] [is_inv_invariant μ] (x : G) :