feat(measure_theory/group/*): various lemmas about invariant measures (#13539)

* Make the `measurable_equiv` argument to `measure_preserving.symm` explicit. This argument is cannot always be deduced from the other explicit arguments (which can be seen form the changes in `src/measure_theory/constructions/pi.lean`).
* From the sphere eversion project
* Required for convolutions

Author: fpvandoorn

src/analysis/complex/cauchy_integral.lean

@@ -189,7 +189,7 @@ begin
   refine (integral2_divergence_prod_of_has_fderiv_within_at_off_countable
       (λ p, -(I • F p)) F (λ p, - (I • F' p)) F' z.re w.im w.re z.im t (hs.preimage e.injective)
       (htc.const_smul _).neg htc (λ p hp, ((htd p hp).const_smul I).neg) htd _).symm,
-  rw [← volume_preserving_equiv_real_prod.symm.integrable_on_comp_preimage
+  rw [← (volume_preserving_equiv_real_prod.symm _).integrable_on_comp_preimage
     (measurable_equiv.measurable_embedding _)] at Hi,
   simpa only [hF'] using Hi.neg
 end

src/dynamics/ergodic/measure_preserving.lean

@@ -56,7 +56,7 @@ protected lemma ae_measurable {f : α → β} (hf : measure_preserving f μa μb
   ae_measurable f μa :=
 hf.1.ae_measurable
 
-lemma symm {e : α ≃ᵐ β} {μa : measure α} {μb : measure β} (h : measure_preserving e μa μb) :
+lemma symm (e : α ≃ᵐ β) {μa : measure α} {μb : measure β} (h : measure_preserving e μa μb) :
   measure_preserving e.symm μb μa :=
 ⟨e.symm.measurable,
   by rw [← h.map_eq, map_map e.symm.measurable e.measurable, e.symm_comp_self, map_id]⟩

src/measure_theory/constructions/pi.lean

@@ -591,7 +591,7 @@ lemma measure_preserving_pi_equiv_pi_subtype_prod {ι : Type u} {α : ι → Typ
     ((measure.pi $ λ i : subtype p, μ i).prod (measure.pi $ λ i, μ i)) :=
 begin
   set e := (measurable_equiv.pi_equiv_pi_subtype_prod α p).symm,
-  suffices : measure_preserving e _ _, from this.symm,
+  refine measure_preserving.symm e _,
   refine ⟨e.measurable, (pi_eq $ λ s hs, _).symm⟩,
   have : e ⁻¹' (pi univ s) =
     (pi univ (λ i : {i // p i}, s i)) ×ˢ (pi univ (λ i : {i // ¬p i}, s i)),
@@ -613,7 +613,7 @@ lemma measure_preserving_pi_fin_succ_above_equiv {n : ℕ} {α : fin (n + 1) →
     ((μ i).prod $ measure.pi $ λ j, μ (i.succ_above j)) :=
 begin
   set e := (measurable_equiv.pi_fin_succ_above_equiv α i).symm,
-  suffices : measure_preserving e _ _, from this.symm,
+  refine measure_preserving.symm e _,
   refine ⟨e.measurable, (pi_eq $ λ s hs, _).symm⟩,
   rw [e.map_apply, i.prod_univ_succ_above _, ← pi_pi, ← prod_prod],
   congr' 1 with ⟨x, f⟩,
@@ -635,7 +635,7 @@ begin
     rw [pi_premeasure, fintype.prod_unique, to_outer_measure_apply, e.symm.map_apply],
     congr' 1, exact e.to_equiv.image_eq_preimage s },
   simp only [measure.pi, outer_measure.pi, this, bounded_by_measure, to_outer_measure_to_measure],
-  exact ((measurable_equiv.fun_unique α β).symm.measurable.measure_preserving _).symm
+  exact (e.symm.measurable.measure_preserving _).symm e.symm
 end
 
 lemma volume_preserving_fun_unique (α : Type u) (β : Type v) [unique α] [measure_space β] :

src/measure_theory/constructions/prod.lean

@@ -557,10 +557,10 @@ end
 
 end measure
 
-namespace measure_preserving
-
 open measure
 
+namespace measure_preserving
+
 variables {δ : Type*} [measurable_space δ] {μa : measure α} {μb : measure β}
   {μc : measure γ} {μd : measure δ}
 
@@ -603,6 +603,34 @@ hf.skew_product this $ filter.eventually_of_forall $ λ _, hg.map_eq
 
 end measure_preserving
 
+namespace quasi_measure_preserving
+
+lemma prod_of_right {f : α × β → γ} {μ : measure α} {ν : measure β} {τ : measure γ}
+  (hf : measurable f) [sigma_finite ν]
+  (h2f : ∀ᵐ x ∂μ, quasi_measure_preserving (λ y, f (x, y)) ν τ) :
+  quasi_measure_preserving f (μ.prod ν) τ :=
+begin
+  refine ⟨hf, _⟩,
+  refine absolutely_continuous.mk (λ s hs h2s, _),
+  simp_rw [map_apply hf hs, prod_apply (hf hs), preimage_preimage,
+    lintegral_congr_ae (h2f.mono (λ x hx, hx.preimage_null h2s)), lintegral_zero],
+end
+
+lemma prod_of_left {α β γ} [measurable_space α] [measurable_space β]
+  [measurable_space γ] {f : α × β → γ} {μ : measure α} {ν : measure β} {τ : measure γ}
+  (hf : measurable f) [sigma_finite μ] [sigma_finite ν]
+  (h2f : ∀ᵐ y ∂ν, quasi_measure_preserving (λ x, f (x, y)) μ τ) :
+  quasi_measure_preserving f (μ.prod ν) τ :=
+begin
+  rw [← prod_swap],
+  convert (quasi_measure_preserving.prod_of_right (hf.comp measurable_swap) h2f).comp
+    ((measurable_swap.measure_preserving (ν.prod μ)).symm measurable_equiv.prod_comm)
+    .quasi_measure_preserving,
+  ext ⟨x, y⟩, refl,
+end
+
+end quasi_measure_preserving
+
 end measure_theory
 
 open measure_theory.measure
@@ -627,6 +655,16 @@ lemma ae_measurable.snd [sigma_finite ν] {f : β → γ}
   (hf : ae_measurable f ν) : ae_measurable (λ (z : α × β), f z.2) (μ.prod ν) :=
 hf.comp_measurable' measurable_snd prod_snd_absolutely_continuous
 
+lemma measure_theory.ae_strongly_measurable.fst {γ} [topological_space γ] [sigma_finite ν]
+  {f : α → γ} (hf : ae_strongly_measurable f μ) :
+  ae_strongly_measurable (λ (z : α × β), f z.1) (μ.prod ν) :=
+hf.comp_measurable' measurable_fst prod_fst_absolutely_continuous
+
+lemma measure_theory.ae_strongly_measurable.snd {γ} [topological_space γ] [sigma_finite ν]
+  {f : β → γ} (hf : ae_strongly_measurable f ν) :
+  ae_strongly_measurable (λ (z : α × β), f z.2) (μ.prod ν) :=
+hf.comp_measurable' measurable_snd prod_snd_absolutely_continuous
+
 /-- The Bochner integral is a.e.-measurable.
   This shows that the integrand of (the right-hand-side of) Fubini's theorem is a.e.-measurable. -/
 lemma measure_theory.ae_strongly_measurable.integral_prod_right' [sigma_finite ν]

src/measure_theory/function/strongly_measurable.lean

@@ -1299,6 +1299,11 @@ lemma comp_measurable {γ : Type*} {mγ : measurable_space γ} {mα : measurable
   ae_strongly_measurable (g ∘ f) μ :=
 hg.comp_ae_measurable hf.ae_measurable
 
+lemma comp_measurable' {γ : Type*} {mγ : measurable_space γ} {mα : measurable_space α} {f : γ → α}
+  {μ : measure γ} {ν : measure α} (hg : ae_strongly_measurable g ν) (hf : measurable f)
+  (h : μ.map f ≪ ν) : ae_strongly_measurable (g ∘ f) μ :=
+(hg.mono' h).comp_measurable hf
+
 lemma is_separable_ae_range (hf : ae_strongly_measurable f μ) :
   ∃ (t : set β), is_separable t ∧ ∀ᵐ x ∂μ, f x ∈ t :=
 begin
@@ -1513,10 +1518,12 @@ lemma apply_continuous_linear_map {φ : α → F →L[𝕜] E}
   ae_strongly_measurable (λ a, φ a v) μ :=
 (continuous_linear_map.apply 𝕜 E v).continuous.comp_ae_strongly_measurable hφ
 
-lemma ae_strongly_measurable_comp₂ (L : E →L[𝕜] F →L[𝕜] G) {f : α → E} {g : α → F}
+lemma _root_.continuous_linear_map.ae_strongly_measurable_comp₂ (L : E →L[𝕜] F →L[𝕜] G)
+  {f : α → E} {g : α → F}
   (hf : ae_strongly_measurable f μ) (hg : ae_strongly_measurable g μ) :
   ae_strongly_measurable (λ x, L (f x) (g x)) μ :=
 L.continuous₂.comp_ae_strongly_measurable $ hf.prod_mk hg
+
 end continuous_linear_map_nondiscrete_normed_field
 
 lemma _root_.ae_strongly_measurable_with_density_iff {E : Type*} [normed_group E] [normed_space ℝ E]

src/measure_theory/group/arithmetic.lean

@@ -57,6 +57,8 @@ class has_measurable_add (M : Type*) [measurable_space M] [has_add M] : Prop :=
 (measurable_const_add : ∀ c : M, measurable ((+) c))
 (measurable_add_const : ∀ c : M, measurable (+ c))
 
+export has_measurable_add (measurable_const_add measurable_add_const)
+
 /-- We say that a type `has_measurable_add` if `uncurry (+)` is a measurable functions.
 For a typeclass assuming measurability of `((+) c)` and `(+ c)` see `has_measurable_add`. -/
 class has_measurable_add₂ (M : Type*) [measurable_space M] [has_add M] : Prop :=
@@ -72,14 +74,15 @@ class has_measurable_mul (M : Type*) [measurable_space M] [has_mul M] : Prop :=
 (measurable_const_mul : ∀ c : M, measurable ((*) c))
 (measurable_mul_const : ∀ c : M, measurable (* c))
 
+export has_measurable_mul (measurable_const_mul measurable_mul_const)
+
 /-- We say that a type `has_measurable_mul` if `uncurry (*)` is a measurable functions.
 For a typeclass assuming measurability of `((*) c)` and `(* c)` see `has_measurable_mul`. -/
 @[to_additive has_measurable_add₂]
 class has_measurable_mul₂ (M : Type*) [measurable_space M] [has_mul M] : Prop :=
 (measurable_mul : measurable (λ p : M × M, p.1 * p.2))
 
 export has_measurable_mul₂ (measurable_mul)
-  has_measurable_mul (measurable_const_mul measurable_mul_const)
 
 section mul
 
@@ -152,9 +155,16 @@ instance pi.has_measurable_mul₂ {ι : Type*} {α : ι → Type*} [∀ i, has_m
 attribute [measurability] measurable.add' measurable.add ae_measurable.add ae_measurable.add'
   measurable.const_add ae_measurable.const_add measurable.add_const ae_measurable.add_const
 
-
 end mul
 
+/-- A version of `measurable_div_const` that assumes `has_measurable_mul` instead of
+  `has_measurable_div`. This can be nice to avoid unnecessary type-class assumptions. -/
+@[to_additive /-" A version of `measurable_sub_const` that assumes `has_measurable_add` instead of
+  `has_measurable_sub`. This can be nice to avoid unnecessary type-class assumptions. "-/]
+lemma measurable_div_const' {G : Type*} [div_inv_monoid G] [measurable_space G]
+  [has_measurable_mul G] (g : G) : measurable (λ h, h / g) :=
+by simp_rw [div_eq_mul_inv, measurable_mul_const]
+
 /-- This class assumes that the map `β × γ → β` given by `(x, y) ↦ x ^ y` is measurable. -/
 class has_measurable_pow (β γ : Type*) [measurable_space β] [measurable_space γ] [has_pow β γ] :=
 (measurable_pow : measurable (λ p : β × γ, p.1 ^ p.2))
@@ -217,6 +227,8 @@ class has_measurable_sub (G : Type*) [measurable_space G] [has_sub G] : Prop :=
 (measurable_const_sub : ∀ c : G, measurable (λ x, c - x))
 (measurable_sub_const : ∀ c : G, measurable (λ x, x - c))
 
+export has_measurable_sub (measurable_const_sub measurable_sub_const)
+
 /-- We say that a type `has_measurable_sub` if `uncurry (-)` is a measurable functions.
 For a typeclass assuming measurability of `((-) c)` and `(- c)` see `has_measurable_sub`. -/
 class has_measurable_sub₂ (G : Type*) [measurable_space G] [has_sub G] : Prop :=
@@ -230,6 +242,8 @@ For a typeclass assuming measurability of `uncurry (/)` see `has_measurable_div
 (measurable_const_div : ∀ c : G₀, measurable ((/) c))
 (measurable_div_const : ∀ c : G₀, measurable (/ c))
 
+export has_measurable_div (measurable_const_div measurable_div_const)
+
 /-- We say that a type `has_measurable_div` if `uncurry (/)` is a measurable functions.
 For a typeclass assuming measurability of `((/) c)` and `(/ c)` see `has_measurable_div`. -/
 @[to_additive has_measurable_sub₂]
@@ -447,9 +461,9 @@ class has_measurable_smul₂ (M α : Type*) [has_scalar M α] [measurable_space
 (measurable_smul : measurable (function.uncurry (•) : M × α → α))
 
 export has_measurable_smul (measurable_const_smul measurable_smul_const)
-  has_measurable_smul₂ (measurable_smul)
+export has_measurable_smul₂ (measurable_smul)
 export has_measurable_vadd (measurable_const_vadd measurable_vadd_const)
-  has_measurable_vadd₂ (measurable_vadd)
+export has_measurable_vadd₂ (measurable_vadd)
 
 @[to_additive]
 instance has_measurable_smul_of_mul (M : Type*) [has_mul M] [measurable_space M]

src/measure_theory/group/fundamental_domain.lean

@@ -119,12 +119,12 @@ h.pairwise_ae_disjoint.mono $ λ g₁ g₂ H, hν H
     end }
 
 @[to_additive] lemma image_of_equiv (h : is_fundamental_domain G s μ)
-  (f : measurable_equiv α α) (hfμ : measure_preserving f μ μ)
+  (f : α ≃ᵐ α) (hfμ : measure_preserving f μ μ)
   (e : equiv.perm G) (hef : ∀ g, semiconj f ((•) (e g)) ((•) g)) :
   is_fundamental_domain G (f '' s) μ :=
 begin
   rw f.image_eq_preimage,
-  refine h.preimage_of_equiv hfμ.symm.quasi_measure_preserving e.symm.bijective (λ g x, _),
+  refine h.preimage_of_equiv (hfμ.symm f).quasi_measure_preserving e.symm.bijective (λ g x, _),
   rcases f.surjective x with ⟨x, rfl⟩,
   rw [← hef _ _, f.symm_apply_apply, f.symm_apply_apply, e.apply_symm_apply]
 end

src/measure_theory/group/integration.lean

@@ -5,6 +5,7 @@ Authors: Floris van Doorn
 -/
 import measure_theory.integral.bochner
 import measure_theory.group.measure
+import measure_theory.group.action
 
 /-!
 # Integration on Groups
@@ -18,7 +19,7 @@ namespace measure_theory
 open measure topological_space
 open_locale ennreal
 
-variables {𝕜 G E F : Type*} [measurable_space G]
+variables {𝕜 M α G E F : Type*} [measurable_space G]
 variables [normed_group E] [normed_space ℝ E] [complete_space E] [normed_group F]
 variables {μ : measure G} {f : G → E} {g : G}
 
@@ -68,10 +69,15 @@ begin
   simp [map_mul_right_eq_self μ g]
 end
 
+@[simp, to_additive]
+lemma lintegral_div_right_eq_self [is_mul_right_invariant μ] (f : G → ℝ≥0∞) (g : G) :
+  ∫⁻ x, f (x / g) ∂μ = ∫⁻ x, f x ∂μ :=
+by simp_rw [div_eq_mul_inv, lintegral_mul_right_eq_self f g⁻¹]
+
 /-- Translating a function by left-multiplication does not change its integral with respect to a
 left-invariant measure. -/
-@[to_additive "Translating a function by left-addition does not change its integral with respect to
-a left-invariant measure."]
+@[simp, to_additive "Translating a function by left-addition does not change its integral with
+  respect to a left-invariant measure."]
 lemma integral_mul_left_eq_self [is_mul_left_invariant μ] (f : G → E) (g : G) :
   ∫ x, f (g * x) ∂μ = ∫ x, f x ∂μ :=
 begin
@@ -82,8 +88,8 @@ end
 
 /-- Translating a function by right-multiplication does not change its integral with respect to a
 right-invariant measure. -/
-@[to_additive "Translating a function by right-addition does not change its integral with respect to
-a right-invariant measure."]
+@[simp, to_additive "Translating a function by right-addition does not change its integral with
+  respect to a right-invariant measure."]
 lemma integral_mul_right_eq_self [is_mul_right_invariant μ] (f : G → E) (g : G) :
   ∫ x, f (x * g) ∂μ = ∫ x, f x ∂μ :=
 begin
@@ -92,6 +98,11 @@ begin
   rw [← h_mul.integral_map, map_mul_right_eq_self]
 end
 
+@[simp, to_additive]
+lemma integral_div_right_eq_self [is_mul_right_invariant μ] (f : G → E) (g : G) :
+  ∫ x, f (x / g) ∂μ = ∫ x, f x ∂μ :=
+by simp_rw [div_eq_mul_inv, integral_mul_right_eq_self f g⁻¹]
+
 /-- 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 "If some left-translate of a function negates it, then the integral of the function
@@ -139,14 +150,39 @@ begin
   { exact (measurable_id'.const_mul g⁻¹).inv.ae_measurable }
 end
 
-@[to_additive]
+@[simp, to_additive]
+lemma integrable_comp_div_left (f : G → F)
+  [is_inv_invariant μ] [is_mul_left_invariant μ] (g : G) :
+  integrable (λ t, f (g / t)) μ ↔ integrable f μ :=
+begin
+  refine ⟨λ h, _, λ h, h.comp_div_left g⟩,
+  convert h.comp_inv.comp_mul_left g⁻¹,
+  simp_rw [div_inv_eq_mul, mul_inv_cancel_left]
+end
+
+@[simp, to_additive]
 lemma integral_div_left_eq_self (f : G → E) (μ : measure G) [is_inv_invariant μ]
   [is_mul_left_invariant μ] (x' : G) : ∫ x, f (x' / x) ∂μ = ∫ x, f x ∂μ :=
 by simp_rw [div_eq_mul_inv, integral_inv_eq_self (λ x, f (x' * x)) μ,
   integral_mul_left_eq_self f x']
 
 end measurable_mul
 
+section smul
+
+variables [group G] [measurable_space α] [mul_action G α] [has_measurable_smul G α]
+
+@[simp, to_additive]
+lemma integral_smul_eq_self {μ : measure α} [smul_invariant_measure G α μ] (f : α → E) {g : G} :
+  ∫ x, f (g • x) ∂μ = ∫ x, f x ∂μ :=
+begin
+  have h : measurable_embedding (λ x : α, g • x) :=
+  (measurable_equiv.smul g).measurable_embedding,
+  rw [← h.integral_map, map_smul]
+end
+
+end smul
+
 
 section topological_group
 

src/measure_theory/group/measurable_equiv.lean

@@ -160,4 +160,18 @@ def inv (G) [measurable_space G] [has_involutive_inv G] [has_measurable_inv G] :
 lemma symm_inv {G} [measurable_space G] [has_involutive_inv G] [has_measurable_inv G] :
   (inv G).symm = inv G := rfl
 
+/-- `equiv.div_right` as a `measurable_equiv`. -/
+@[to_additive /-" `equiv.sub_right` as a `measurable_equiv` "-/]
+def div_right [has_measurable_mul G] (g : G) : G ≃ᵐ G :=
+{ to_equiv := equiv.div_right g,
+  measurable_to_fun := measurable_div_const' g,
+  measurable_inv_fun := measurable_mul_const g }
+
+/-- `equiv.div_left` as a `measurable_equiv` -/
+@[to_additive /-" `equiv.sub_left` as a `measurable_equiv` "-/]
+def div_left [has_measurable_mul G] [has_measurable_inv G] (g : G) : G ≃ᵐ G :=
+{ to_equiv := equiv.div_left g,
+  measurable_to_fun := measurable_id.const_div g,
+  measurable_inv_fun := measurable_inv.mul_const g }
+
 end measurable_equiv