feat(measure_theory/group): add measures invariant under inversion/negation (#11954)

* Define measures invariant under `inv` or `neg`
* Prove lemmas about measures invariant under `inv` similar to the lemmas about measures invariant under `mul`
* Also provide more `pi` instances in `arithmetic`.
* Rename some `integral_zero...` lemmas to `integral_eq_zero...`
* Reformulate `pi.is_mul_left_invariant_volume` using nondependent functions, so that type class inference can find it for `ι → ℝ`)
* Add some more integration lemmas, also for multiplication

Author: fpvandoorn

src/analysis/fourier.lean

@@ -205,7 +205,7 @@ begin
   have hij : -i + j ≠ 0,
   { rw add_comm,
     exact sub_ne_zero.mpr (ne.symm h) },
-  exact integral_zero_of_mul_left_eq_neg (fourier_add_half_inv_index hij)
+  exact integral_eq_zero_of_mul_left_eq_neg (fourier_add_half_inv_index hij)
 end
 
 end monomials

src/measure_theory/constructions/pi.lean

@@ -539,13 +539,21 @@ end
   [∀ 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]
+  have h : has_mul.mul x ⁻¹' (pi univ s) = set.pi univ (λ i, (λ y, x i * y) ⁻¹' s i),
+  { ext, simp },
+  simp_rw [measure.map_apply (measurable_const_mul x) (measurable_set.univ_pi_fintype hs), h,
+    pi_pi, measure_preimage_mul]
 end
 
+@[to_additive] instance pi.is_inv_invariant [∀ i, group (α i)] [∀ i, has_measurable_inv (α i)]
+  [∀ i, is_inv_invariant (μ i)] : is_inv_invariant (measure.pi μ) :=
+begin
+  refine ⟨(measure.pi_eq (λ s hs, _)).symm⟩,
+  have A : has_inv.inv ⁻¹' (pi univ s) = set.pi univ (λ i, has_inv.inv ⁻¹' s i),
+  { ext, simp },
+  simp_rw [measure.inv, measure.map_apply measurable_inv (measurable_set.univ_pi_fintype hs), A,
+    pi_pi, measure_preimage_inv]
+end
 
 end measure
 instance measure_space.pi [Π i, measure_space (α i)] : measure_space (Π i, α i) :=
@@ -571,13 +579,24 @@ lemma volume_pi_closed_ball [Π i, measure_space (α i)] [∀ i, sigma_finite (v
 measure.pi_closed_ball _ _ hr
 
 open measure
+/-- We intentionally restrict this only to the nondependent function space, since type-class
+inference cannot find an instance for `ι → ℝ` when this is stated for dependent function spaces. -/
 @[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)) :=
+instance pi.is_mul_left_invariant_volume {α} [group α] [measure_space α]
+  [sigma_finite (volume : measure α)]
+  [has_measurable_mul α] [is_mul_left_invariant (volume : measure α)] :
+  is_mul_left_invariant (volume : measure (ι → α)) :=
 pi.is_mul_left_invariant _
 
+/-- We intentionally restrict this only to the nondependent function space, since type-class
+inference cannot find an instance for `ι → ℝ` when this is stated for dependent function spaces. -/
+@[to_additive]
+instance pi.is_inv_invariant_volume {α} [group α] [measure_space α]
+  [sigma_finite (volume : measure α)]
+  [has_measurable_inv α] [is_inv_invariant (volume : measure α)] :
+  is_inv_invariant (volume : measure (ι → α)) :=
+pi.is_inv_invariant _
+
 /-!
 ### Measure preserving equivalences
 

src/measure_theory/function/l1_space.lean

@@ -486,6 +486,10 @@ lemma integrable_map_measure [opens_measurable_space β] {f : α → δ} {g : δ
   integrable g (measure.map f μ) ↔ integrable (g ∘ f) μ :=
 by { simp_rw ← mem_ℒp_one_iff_integrable, exact mem_ℒp_map_measure_iff hg hf, }
 
+lemma integrable.comp_measurable [opens_measurable_space β] {f : α → δ} {g : δ → β}
+  (hg : integrable g (measure.map f μ)) (hf : measurable f) : integrable (g ∘ f) μ :=
+(integrable_map_measure hg.ae_measurable hf).mp hg
+
 lemma _root_.measurable_embedding.integrable_map_iff {f : α → δ} (hf : measurable_embedding f)
   {g : δ → β} :
   integrable g (measure.map f μ) ↔ integrable (g ∘ f) μ :=

src/measure_theory/group/arithmetic.lean

@@ -131,17 +131,23 @@ measurable_mul.comp_ae_measurable (hf.prod_mk hg)
 
 omit m
 
+@[priority 100, to_additive]
+instance has_measurable_mul₂.to_has_measurable_mul [has_measurable_mul₂ M] :
+  has_measurable_mul M :=
+⟨λ c, measurable_const.mul measurable_id, λ c, measurable_id.mul measurable_const⟩
+
 @[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⟩
+⟨λ g, measurable_pi_iff.mpr $ λ i, (measurable_pi_apply i).const_mul _,
+ λ g, measurable_pi_iff.mpr $ λ i, (measurable_pi_apply i).mul_const _⟩
 
-@[priority 100, to_additive]
-instance has_measurable_mul₂.to_has_measurable_mul [has_measurable_mul₂ M] :
-  has_measurable_mul M :=
-⟨λ c, measurable_const.mul measurable_id, λ c, measurable_id.mul measurable_const⟩
+@[to_additive pi.has_measurable_add₂]
+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) :=
+⟨measurable_pi_iff.mpr $ λ i, measurable_fst.eval.mul measurable_snd.eval⟩
 
 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
@@ -291,6 +297,19 @@ instance has_measurable_div₂.to_has_measurable_div [has_measurable_div₂ G] :
   has_measurable_div G :=
 ⟨λ c, measurable_const.div measurable_id, λ c, measurable_id.div measurable_const⟩
 
+@[to_additive]
+instance pi.has_measurable_div {ι : Type*} {α : ι → Type*} [∀ i, has_div (α i)]
+  [∀ i, measurable_space (α i)] [∀ i, has_measurable_div (α i)] :
+  has_measurable_div (Π i, α i) :=
+⟨λ g, measurable_pi_iff.mpr $ λ i, (measurable_pi_apply i).const_div _,
+ λ g, measurable_pi_iff.mpr $ λ i, (measurable_pi_apply i).div_const _⟩
+
+@[to_additive pi.has_measurable_sub₂]
+instance pi.has_measurable_div₂ {ι : Type*} {α : ι → Type*} [∀ i, has_div (α i)]
+  [∀ i, measurable_space (α i)] [∀ i, has_measurable_div₂ (α i)] :
+  has_measurable_div₂ (Π i, α i) :=
+⟨measurable_pi_iff.mpr $ λ i, measurable_fst.eval.div measurable_snd.eval⟩
+
 @[measurability]
 lemma measurable_set_eq_fun {m : measurable_space α} {E} [measurable_space E] [add_group E]
   [measurable_singleton_class E] [has_measurable_sub₂ E] {f g : α → E}
@@ -373,6 +392,12 @@ attribute [measurability] measurable.neg ae_measurable.neg
 
 omit m
 
+@[to_additive]
+instance pi.has_measurable_inv {ι : Type*} {α : ι → Type*} [∀ i, has_inv (α i)]
+  [∀ i, measurable_space (α i)] [∀ i, has_measurable_inv (α i)] :
+  has_measurable_inv (Π i, α i) :=
+⟨measurable_pi_iff.mpr $ λ i, (measurable_pi_apply i).inv⟩
+
 @[to_additive] lemma measurable_set.inv {s : set G} (hs : measurable_set s) : measurable_set s⁻¹ :=
 measurable_inv hs
 
@@ -525,6 +550,13 @@ hf.const_smul' c
 
 omit m
 
+@[to_additive]
+instance pi.has_measurable_smul {ι : Type*} {α : ι → Type*} [∀ i, has_scalar M (α i)]
+  [∀ i, measurable_space (α i)] [∀ i, has_measurable_smul M (α i)] :
+  has_measurable_smul M (Π i, α i) :=
+⟨λ g, measurable_pi_iff.mpr $ λ i, (measurable_pi_apply i).const_smul _,
+ λ g, measurable_pi_iff.mpr $ λ i, measurable_smul_const _⟩
+
 end smul
 
 section mul_action

src/measure_theory/group/integration.lean

@@ -18,9 +18,31 @@ namespace measure_theory
 open measure topological_space
 open_locale ennreal
 
-variables {𝕜 G E : Type*} [measurable_space G] {μ : measure G}
+variables {𝕜 G E F : Type*} [measurable_space G]
 variables [normed_group E] [second_countable_topology E] [normed_space ℝ E] [complete_space E]
-  [measurable_space E] [borel_space E]
+variables [measurable_space E] [borel_space E]
+variables [normed_group F] [measurable_space F] [opens_measurable_space F]
+variables {μ : measure G} {f : G → E} {g : G}
+
+section measurable_inv
+
+variables [group G] [has_measurable_inv G]
+
+@[to_additive]
+lemma integrable.comp_inv [is_inv_invariant μ] {f : G → F} (hf : integrable f μ) :
+  integrable (λ t, f t⁻¹) μ :=
+(hf.mono_measure (map_inv_eq_self μ).le).comp_measurable measurable_inv
+
+@[to_additive]
+lemma integral_inv_eq_self (f : G → E) (μ : measure G) [is_inv_invariant μ] :
+  ∫ x, f (x⁻¹) ∂μ = ∫ x, f x ∂μ :=
+begin
+  have h : measurable_embedding (λ x : G, x⁻¹) :=
+  (measurable_equiv.inv G).measurable_embedding,
+  rw [← h.integral_map, map_inv_eq_self]
+end
+
+end measurable_inv
 
 section measurable_mul
 
@@ -71,19 +93,54 @@ 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) :
+lemma integral_eq_zero_of_mul_left_eq_neg [is_mul_left_invariant μ] (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 :=
+lemma integral_eq_zero_of_mul_right_eq_neg [is_mul_right_invariant μ]
+  (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]
 
+@[to_additive]
+lemma integrable.comp_mul_left {f : G → F} [is_mul_left_invariant μ] (hf : integrable f μ)
+  (g : G) : integrable (λ t, f (g * t)) μ :=
+(hf.mono_measure (map_mul_left_eq_self μ g).le).comp_measurable $ measurable_const_mul g
+
+@[to_additive]
+lemma integrable.comp_mul_right {f : G → F} [is_mul_right_invariant μ] (hf : integrable f μ)
+  (g : G) : integrable (λ t, f (t * g)) μ :=
+(hf.mono_measure (map_mul_right_eq_self μ g).le).comp_measurable $ measurable_mul_const g
+
+@[to_additive]
+lemma integrable.comp_div_right {f : G → F} [is_mul_right_invariant μ] (hf : integrable f μ)
+  (g : G) : integrable (λ t, f (t / g)) μ :=
+by { simp_rw [div_eq_mul_inv], exact hf.comp_mul_right g⁻¹ }
+
+variables [has_measurable_inv G]
+
+@[to_additive]
+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_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_measurable },
+  exact (measurable_id'.const_mul g⁻¹).inv
+end
+
+@[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
 
 

src/measure_theory/group/measure.lean

@@ -104,7 +104,15 @@ end mul
 
 section group
 
-variables [group G] [has_measurable_mul G]
+variables [group G]
+
+@[to_additive]
+lemma map_div_right_eq_self (μ : measure G) [is_mul_right_invariant μ] (g : G) :
+  map (/ g) μ = μ :=
+by simp_rw [div_eq_mul_inv, map_mul_right_eq_self μ g⁻¹]
+
+
+variables [has_measurable_mul G]
 
 /-- We shorten this from `measure_preimage_mul_left`, since left invariant is the preferred option
   for measures in this formalization. -/
@@ -131,25 +139,59 @@ namespace measure
 protected def inv [has_inv G] (μ : measure G) : measure G :=
 measure.map inv μ
 
-variables [group G] [has_measurable_inv G]
+/-- A measure is invariant under negation if `- μ = μ`. Equivalently, this means that for all
+measurable `A` we have `μ (- A) = μ A`, where `- A` is the pointwise negation of `A`. -/
+class is_neg_invariant [has_neg G] (μ : measure G) : Prop :=
+(neg_eq_self : μ.neg = μ)
 
-@[to_additive]
+/-- A measure is invariant under inversion if `μ⁻¹ = μ`. Equivalently, this means that for all
+measurable `A` we have `μ (A⁻¹) = μ A`, where `A⁻¹` is the pointwise inverse of `A`. -/
+@[to_additive] class is_inv_invariant [has_inv G] (μ : measure G) : Prop :=
+(inv_eq_self : μ.inv = μ)
+
+section inv
+
+variables [has_inv G]
+
+@[simp, to_additive]
+lemma inv_eq_self (μ : measure G) [is_inv_invariant μ] : μ.inv = μ :=
+is_inv_invariant.inv_eq_self
+
+@[simp, to_additive]
+lemma map_inv_eq_self (μ : measure G) [is_inv_invariant μ] : map has_inv.inv μ = μ :=
+is_inv_invariant.inv_eq_self
+
+end inv
+
+section has_involutive_inv
+
+variables [has_involutive_inv G] [has_measurable_inv G]
+
+@[simp, to_additive]
 lemma inv_apply (μ : measure G) (s : set G) : μ.inv s = μ s⁻¹ :=
 (measurable_equiv.inv G).map_apply s
 
-@[simp, to_additive] protected lemma inv_inv (μ : measure G) : μ.inv.inv = μ :=
+@[simp, to_additive]
+protected lemma inv_inv (μ : measure G) : μ.inv.inv = μ :=
 (measurable_equiv.inv G).map_symm_map
 
-end measure
+@[simp, to_additive]
+lemma measure_inv (μ : measure G) [is_inv_invariant μ] (A : set G) : μ A⁻¹ = μ A :=
+by rw [← inv_apply, inv_eq_self]
 
-section inv
-variables [group G] [has_measurable_inv G] {μ : measure G}
+@[to_additive]
+lemma measure_preimage_inv (μ : measure G) [is_inv_invariant μ] (A : set G) :
+  μ (has_inv.inv ⁻¹' A) = μ A :=
+μ.measure_inv A
 
 @[to_additive]
-instance [sigma_finite μ] : sigma_finite μ.inv :=
+instance (μ : measure G) [sigma_finite μ] : sigma_finite μ.inv :=
 (measurable_equiv.inv G).sigma_finite_map ‹_›
 
-variables [has_measurable_mul G]
+end has_involutive_inv
+
+section mul_inv
+variables [group G] [has_measurable_mul G] [has_measurable_inv G] {μ : measure G}
 
 @[to_additive]
 instance [is_mul_left_invariant μ] : is_mul_right_invariant μ.inv :=
@@ -171,9 +213,28 @@ begin
     map_map measurable_inv (measurable_mul_const g⁻¹), function.comp, mul_inv_rev, inv_inv]
 end
 
-end inv
+@[to_additive]
+lemma map_div_left_eq_self (μ : measure G) [is_inv_invariant μ] [is_mul_left_invariant μ] (g : G) :
+  map (λ 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
+end
 
-section group
+@[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
+
+end mul_inv
+
+end measure
+
+section topological_group
 
 variables [topological_space G] [borel_space G] {μ : measure G}
 variables [group G] [topological_group G]
@@ -263,7 +324,7 @@ 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
 
-end group
+end topological_group
 
 section comm_group
 

src/measure_theory/integral/bochner.lean

@@ -975,14 +975,20 @@ begin
     rw [this, hfi], refl }
 end
 
+lemma integral_norm_eq_lintegral_nnnorm {G} [normed_group G] [measurable_space G]
+  [opens_measurable_space G] {f : α → G} (hf : ae_measurable f μ) :
+  ∫ x, ∥f x∥ ∂μ = ennreal.to_real ∫⁻ x, ∥f x∥₊ ∂μ :=
+begin
+  rw integral_eq_lintegral_of_nonneg_ae _ hf.norm,
+  { simp_rw [of_real_norm_eq_coe_nnnorm], },
+  { refine ae_of_all _ _, simp_rw [pi.zero_apply, norm_nonneg, imp_true_iff] },
+end
+
 lemma of_real_integral_norm_eq_lintegral_nnnorm {G} [normed_group G] [measurable_space G]
   [opens_measurable_space G] {f : α → G} (hf : integrable f μ) :
   ennreal.of_real ∫ x, ∥f x∥ ∂μ = ∫⁻ x, ∥f x∥₊ ∂μ :=
-begin
-  rw integral_eq_lintegral_of_nonneg_ae _ hf.1.norm,
-  { simp_rw [of_real_norm_eq_coe_nnnorm, ennreal.of_real_to_real (lt_top_iff_ne_top.mp hf.2)], },
-  { refine ae_of_all _ _, simp, },
-end
+by rw [integral_norm_eq_lintegral_nnnorm hf.ae_measurable,
+    ennreal.of_real_to_real (lt_top_iff_ne_top.mp hf.2)]
 
 lemma integral_eq_integral_pos_part_sub_integral_neg_part {f : α → ℝ} (hf : integrable f μ) :
   ∫ a, f a ∂μ = (∫ a, real.to_nnreal (f a) ∂μ) - (∫ a, real.to_nnreal (-f a) ∂μ) :=