feat(measure_theory/haar_measure): Prove uniqueness (#5663)

Prove the uniqueness of Haar measure (up to a scalar) following  *Measure Theory* by Paul Halmos. This proof seems to contain an omission which we fix by adding an extra hypothesis to an intermediate lemma.
Add some lemmas about left invariant regular measures.
We add the file `measure_theory.prod_group` which contain various measure-theoretic properties of products of topological groups, needed for the uniqueness.
We add `@[to_additive]` to some declarations in `measure_theory`, but leave it out for many because of #4210. This causes some renamings in concepts, like `is_left_invariant` -> `is_mul_left_invariant` and `measure.conj` -> `measure.inv` (though a better naming suggestion for this one is welcome).

Author: fpvandoorn

docs/references.bib

@@ -97,6 +97,15 @@ @book {gouvea1997
        URL = {https://doi.org/10.1007/978-3-642-59058-0},
 }
 
+@book{halmos2013measure,
+  title     = {Measure theory},
+  author    = {Halmos, Paul R},
+  volume    = {18},
+  year      = {1950},
+  publisher = {Springer},
+  isbn      = {0-387-90088-8}
+}
+
 @article {huneke2002,
     AUTHOR = {Huneke, Craig},
      TITLE = {The Friendship Theorem},

src/measure_theory/borel_space.lean

@@ -1203,7 +1203,7 @@ end normed_space
 namespace measure_theory
 namespace measure
 
-variables [topological_space α]
+variables [topological_space α] {μ : measure α}
 
 /-- A measure `μ` is regular if
   - it is finite on all compact sets;
@@ -1218,16 +1218,20 @@ structure regular (μ : measure α) : Prop :=
 
 namespace regular
 
-lemma outer_regular_eq {μ : measure α} (hμ : μ.regular) {{A : set α}}
+lemma outer_regular_eq (hμ : μ.regular) {{A : set α}}
   (hA : is_measurable A) : (⨅ (U : set α) (h : is_open U) (h2 : A ⊆ U), μ U) = μ A :=
 le_antisymm (hμ.outer_regular hA) $ le_infi $ λ s, le_infi $ λ hs, le_infi $ λ h2s, μ.mono h2s
 
-lemma inner_regular_eq {μ : measure α} (hμ : μ.regular) {{U : set α}}
+lemma inner_regular_eq (hμ : μ.regular) {{U : set α}}
   (hU : is_open U) : (⨆ (K : set α) (h : is_compact K) (h2 : K ⊆ U), μ K) = μ U :=
 le_antisymm (supr_le $ λ s, supr_le $ λ hs, supr_le $ λ h2s, μ.mono h2s) (hμ.inner_regular hU)
 
+lemma exists_compact_not_null (hμ : regular μ) : (∃ K, is_compact K ∧ μ K ≠ 0) ↔ μ ≠ 0 :=
+by simp_rw [ne.def, ← measure_univ_eq_zero, ← hμ.inner_regular_eq is_open_univ,
+    ennreal.supr_eq_zero, not_forall, exists_prop, subset_univ, true_and]
+
 protected lemma map [opens_measurable_space α] [measurable_space β] [topological_space β]
-  [t2_space β] [borel_space β] {μ : measure α} (hμ : μ.regular) (f : α ≃ₜ β) :
+  [t2_space β] [borel_space β] (hμ : μ.regular) (f : α ≃ₜ β) :
   (measure.map f μ).regular :=
 begin
   have hf := f.continuous.measurable,
@@ -1249,7 +1253,7 @@ begin
     rw [map_apply hf hK.is_measurable] }
 end
 
-protected lemma smul {μ : measure α} (hμ : μ.regular) {x : ennreal} (hx : x < ⊤) :
+protected lemma smul (hμ : μ.regular) {x : ennreal} (hx : x < ⊤) :
   (x • μ).regular :=
 begin
   split,
@@ -1264,6 +1268,15 @@ begin
     rw [ennreal.mul_supr], refl' }
 end
 
+/-- A regular measure in a σ-compact space is σ-finite. -/
+protected lemma sigma_finite [opens_measurable_space α] [t2_space α] [sigma_compact_space α]
+  (hμ : regular μ) : sigma_finite μ :=
+⟨{ set := compact_covering α,
+  set_mem := λ n, (is_compact_compact_covering α n).is_measurable,
+  finite := λ n, hμ.lt_top_of_is_compact $ is_compact_compact_covering α n,
+  spanning := Union_compact_covering α }⟩
+
+
 end regular
 
 end measure

src/measure_theory/content.lean

@@ -141,12 +141,15 @@ begin
   apply h,
 end
 
-lemma is_left_invariant_inner_content [group G] [topological_group G] {μ : compacts G → ennreal}
+@[to_additive]
+lemma is_mul_left_invariant_inner_content [group G] [topological_group G] {μ : compacts G → ennreal}
   (h : ∀ (g : G) {K : compacts G}, μ (K.map _ $ continuous_mul_left g) = μ K) (g : G)
   (U : opens G) : inner_content μ (U.comap $ continuous_mul_left g) = inner_content μ U :=
 by convert inner_content_comap (homeomorph.mul_left g) (λ K, h g) U
 
-lemma inner_content_pos [t2_space G] [group G] [topological_group G] {μ : compacts G → ennreal}
+-- @[to_additive] (fails for now)
+lemma inner_content_pos_of_is_mul_left_invariant [t2_space G] [group G] [topological_group G]
+  {μ : compacts G → ennreal}
   (h1 : μ ⊥ = 0)
   (h2 : ∀ (K₁ K₂ : compacts G), μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂)
   (h3 : ∀ (g : G) {K : compacts G}, μ (K.map _ $ continuous_mul_left g) = μ K)
@@ -162,7 +165,7 @@ begin
   refine (le_inner_content _ _ this).trans _,
   refine (rel_supr_sum (inner_content μ) (inner_content_empty h1) (≤)
     (inner_content_Sup_nat h1 h2) _ _).trans _,
-  simp only [is_left_invariant_inner_content h3, finset.sum_const, nsmul_eq_mul, le_refl]
+  simp only [is_mul_left_invariant_inner_content h3, finset.sum_const, nsmul_eq_mul, le_refl]
 end
 
 lemma inner_content_mono' {μ : compacts G → ennreal} ⦃U V : set G⦄
@@ -228,7 +231,8 @@ begin
   intros s hs, convert inner_content_comap f h ⟨s, hs⟩
 end
 
-lemma is_left_invariant_of_content [group G] [topological_group G]
+@[to_additive]
+lemma is_mul_left_invariant_of_content [group G] [topological_group G]
   (h : ∀ (g : G) {K : compacts G}, μ (K.map _ $ continuous_mul_left g) = μ K) (g : G)
   (A : set G) : of_content μ h1 ((λ h, g * h) ⁻¹' A) = of_content μ h1 A :=
 by convert of_content_preimage h2 (homeomorph.mul_left g) (λ K, h g) A
@@ -243,11 +247,13 @@ begin
   apply inner_content_mono'
 end
 
-lemma of_content_pos_of_is_open [group G] [topological_group G]
+-- @[to_additive] (fails for now)
+lemma of_content_pos_of_is_mul_left_invariant [group G] [topological_group G]
   (h3 : ∀ (g : G) {K : compacts G}, μ (K.map _ $ continuous_mul_left g) = μ K)
   (K : compacts G) (hK : 0 < μ K) {U : set G} (h1U : is_open U) (h2U : U.nonempty) :
   0 < of_content μ h1 U :=
-by { convert inner_content_pos h1 h2 h3 K hK ⟨U, h1U⟩ h2U, exact of_content_opens h2 ⟨U, h1U⟩ }
+by { convert inner_content_pos_of_is_mul_left_invariant h1 h2 h3 K hK ⟨U, h1U⟩ h2U,
+     exact of_content_opens h2 ⟨U, h1U⟩ }
 
 end outer_measure
 end measure_theory

src/measure_theory/group.lean

@@ -3,19 +3,21 @@ 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.borel_space
+import measure_theory.integration
+
 /-!
 # Measures on Groups
 
 We develop some properties of measures on (topological) groups
 
-* We define properties on measures: left and right invariant measures
-* We define the conjugate `A ↦ μ (A⁻¹)` of a measure `μ`, and show that it is right invariant iff
-  `μ` is left invariant
+* We define properties on measures: left and right invariant measures.
+* We define the measure `μ.inv : A ↦ μ(A⁻¹)` and show that it is right invariant iff
+  `μ` is left invariant.
 -/
+
 noncomputable theory
 
-open has_inv set function
+open has_inv set function measure_theory.measure
 
 namespace measure_theory
 
@@ -25,16 +27,26 @@ section
 
 variables [measurable_space G] [has_mul G]
 
-/-- A measure `μ` on a topological group is left invariant if
-  for all measurable sets `s` and all `g`, we have `μ (gs) = μ s`,
-  where `gs` denotes the translate of `s` by left multiplication with `g`. -/
-def is_left_invariant (μ : set G → ennreal) : Prop :=
+/-- A measure `μ` on a topological group is left invariant
+  if the measure of left translations of a set are equal to the measure of the set itself.
+  To left translate sets we use preimage under left multiplication,
+  since preimages are nicer to work with than images. -/
+@[to_additive "A measure on a topological group is left invariant
+  if the measure of left translations of a set are equal to the measure of the set itself.
+  To left translate sets we use preimage under left addition,
+  since preimages are nicer to work with than images."]
+def is_mul_left_invariant (μ : set G → ennreal) : Prop :=
 ∀ (g : G) {A : set G} (h : is_measurable A), μ ((λ h, g * h) ⁻¹' A) = μ A
 
-/-- A measure `μ` on a topological group is right invariant if
-  for all measurable sets `s` and all `g`, we have `μ (sg) = μ s`,
-  where `sg` denotes the translate of `s` by right multiplication with `g`. -/
-def is_right_invariant (μ : set G → ennreal) : Prop :=
+/-- A measure `μ` on a topological group is right invariant
+  if the measure of right translations of a set are equal to the measure of the set itself.
+  To right translate sets we use preimage under right multiplication,
+  since preimages are nicer to work with than images. -/
+@[to_additive "A measure on a topological group is right invariant
+  if the measure of right translations of a set are equal to the measure of the set itself.
+  To right translate sets we use preimage under right addition,
+  since preimages are nicer to work with than images."]
+def is_mul_right_invariant (μ : set G → ennreal) : Prop :=
 ∀ (g : G) {A : set G} (h : is_measurable A), μ ((λ h, h * g) ⁻¹' A) = μ A
 
 end
@@ -43,73 +55,160 @@ namespace measure
 
 variables [measurable_space G]
 
+@[to_additive]
 lemma map_mul_left_eq_self [topological_space G] [has_mul G] [has_continuous_mul G] [borel_space G]
-  {μ : measure G} : (∀ g, measure.map ((*) g) μ = μ) ↔ is_left_invariant μ :=
+  {μ : measure G} : (∀ g, measure.map ((*) g) μ = μ) ↔ is_mul_left_invariant μ :=
 begin
   apply forall_congr, intro g, rw [measure.ext_iff], apply forall_congr, intro A,
   apply forall_congr, intro hA, rw [map_apply (measurable_mul_left g) hA]
 end
 
+@[to_additive]
 lemma map_mul_right_eq_self [topological_space G] [has_mul G] [has_continuous_mul G] [borel_space G]
-  {μ : measure G} : (∀ g, measure.map (λ h, h * g) μ = μ) ↔ is_right_invariant μ :=
+  {μ : measure G} : (∀ g, measure.map (λ h, h * g) μ = μ) ↔ is_mul_right_invariant μ :=
 begin
   apply forall_congr, intro g, rw [measure.ext_iff], apply forall_congr, intro A,
   apply forall_congr, intro hA, rw [map_apply (measurable_mul_right g) hA]
 end
 
-/-- The conjugate of a measure on a topological group.
-  Defined to be `A ↦ μ (A⁻¹)`, where `A⁻¹` is the pointwise inverse of `A`. -/
-protected def conj [group G] (μ : measure G) : measure G :=
+/-- The measure `A ↦ μ (A⁻¹)`, where `A⁻¹` is the pointwise inverse of `A`. -/
+@[to_additive "The measure `A ↦ μ (- A)`, where `- A` is the pointwise negation of `A`."]
+protected def inv [has_inv G] (μ : measure G) : measure G :=
 measure.map inv μ
 
 variables [group G] [topological_space G] [topological_group G] [borel_space G]
 
-lemma conj_apply (μ : measure G) {s : set G} (hs : is_measurable s) :
-  μ.conj s = μ s⁻¹ :=
-by { unfold measure.conj, rw [measure.map_apply measurable_inv hs, inv_preimage] }
+@[to_additive]
+lemma inv_apply (μ : measure G) {s : set G} (hs : is_measurable s) :
+  μ.inv s = μ s⁻¹ :=
+by { unfold measure.inv, rw [measure.map_apply measurable_inv hs, inv_preimage] }
 
-@[simp] lemma conj_conj (μ : measure G) : μ.conj.conj = μ :=
+@[simp, to_additive] protected lemma inv_inv (μ : measure G) : μ.inv.inv = μ :=
 begin
-  ext1 s hs, rw [μ.conj.conj_apply hs, μ.conj_apply, set.inv_inv], exact measurable_inv hs
+  ext1 s hs, rw [μ.inv.inv_apply hs, μ.inv_apply, set.inv_inv],
+  exact measurable_inv hs
 end
 
 variables {μ : measure G}
 
-lemma regular.conj [t2_space G] (hμ : μ.regular) : μ.conj.regular :=
+@[to_additive]
+lemma regular.inv [t2_space G] (hμ : μ.regular) : μ.inv.regular :=
 hμ.map (homeomorph.inv G)
 
 end measure
 
-section conj
+section inv
 variables [measurable_space G] [group G] [topological_space G] [topological_group G] [borel_space G]
   {μ : measure G}
 
-@[simp] lemma regular_conj_iff [t2_space G] : μ.conj.regular ↔ μ.regular :=
-by { refine ⟨λ h, _, measure.regular.conj⟩, rw ←μ.conj_conj, exact measure.regular.conj h }
+@[simp, to_additive] lemma regular_inv_iff [t2_space G] : μ.inv.regular ↔ μ.regular :=
+by { refine ⟨λ h, _, measure.regular.inv⟩, rw ←μ.inv_inv, exact measure.regular.inv h }
 
-lemma is_right_invariant_conj' (h : is_left_invariant μ) :
-  is_right_invariant μ.conj :=
+@[to_additive]
+lemma is_mul_left_invariant.inv (h : is_mul_left_invariant μ) :
+  is_mul_right_invariant μ.inv :=
 begin
-  intros g A hA, rw [μ.conj_apply (measurable_mul_right g hA), μ.conj_apply hA],
+  intros g A hA,
+  rw [μ.inv_apply (measurable_mul_right g hA), μ.inv_apply hA],
   convert h g⁻¹ (measurable_inv hA) using 2,
   simp only [←preimage_comp, ← inv_preimage],
-  apply preimage_congr, intro h, simp only [mul_inv_rev, comp_app, inv_inv]
+  apply preimage_congr,
+  intro h,
+  simp only [mul_inv_rev, comp_app, inv_inv]
 end
 
-lemma is_left_invariant_conj' (h : is_right_invariant μ) : is_left_invariant μ.conj :=
+@[to_additive]
+lemma is_mul_right_invariant.inv (h : is_mul_right_invariant μ) : is_mul_left_invariant μ.inv :=
 begin
-  intros g A hA, rw [μ.conj_apply (measurable_mul_left g hA), μ.conj_apply hA],
+  intros g A hA,
+  rw [μ.inv_apply (measurable_mul_left g hA), μ.inv_apply hA],
   convert h g⁻¹ (measurable_inv hA) using 2,
   simp only [←preimage_comp, ← inv_preimage],
-  apply preimage_congr, intro h, simp only [mul_inv_rev, comp_app, inv_inv]
+  apply preimage_congr,
+  intro h,
+  simp only [mul_inv_rev, comp_app, inv_inv]
 end
 
-@[simp] lemma is_right_invariant_conj : is_right_invariant μ.conj ↔ is_left_invariant μ :=
-by { refine ⟨λ h, _, is_right_invariant_conj'⟩, rw ←μ.conj_conj, exact is_left_invariant_conj' h }
+@[simp, to_additive]
+lemma is_mul_right_invariant_inv : is_mul_right_invariant μ.inv ↔ is_mul_left_invariant μ :=
+⟨λ h, by { rw ← μ.inv_inv, exact h.inv }, λ h, h.inv⟩
+
+@[simp, to_additive]
+lemma is_mul_left_invariant_inv : is_mul_left_invariant μ.inv ↔ is_mul_right_invariant μ :=
+⟨λ h, by { rw ← μ.inv_inv, exact h.inv }, λ h, h.inv⟩
+
+end inv
 
-@[simp] lemma is_left_invariant_conj : is_left_invariant μ.conj ↔ is_right_invariant μ :=
-by { refine ⟨λ h, _, is_left_invariant_conj'⟩, rw ←μ.conj_conj, exact is_right_invariant_conj' h }
+variables [measurable_space G] [topological_space G] [borel_space G] {μ : measure G}
+
+section group
+
+variables [group G] [topological_group G]
+
+/-! Properties of regular left invariant measures -/
+@[to_additive measure_theory.measure.is_add_left_invariant.null_iff_empty]
+lemma is_mul_left_invariant.null_iff_empty (hμ : μ.regular) (h2μ : is_mul_left_invariant μ)
+  (h3μ : μ ≠ 0) {s : set G} (hs : is_open s) : μ s = 0 ↔ s = ∅ :=
+begin
+  obtain ⟨K, hK, h2K⟩ := hμ.exists_compact_not_null.mpr h3μ,
+  refine ⟨λ h, _, λ h, by simp [h]⟩,
+  apply classical.by_contradiction, -- `by_contradiction` is very slow
+  refine mt (λ h2s, _) h2K,
+  rw [← ne.def, ne_empty_iff_nonempty] at h2s, cases h2s with y hy,
+  obtain ⟨t, -, h1t, h2t⟩ := hK.elim_finite_subcover_image
+    (show ∀ x ∈ @univ G, is_open ((λ y, x * y) ⁻¹' s),
+      from λ x _, (continuous_mul_left x).is_open_preimage _ hs) _,
+  { rw [← nonpos_iff_eq_zero],
+    refine (measure_mono h2t).trans _,
+    refine (measure_bUnion_le h1t.countable _).trans_eq _,
+    simp_rw [h2μ _ hs.is_measurable], rw [h, tsum_zero] },
+  { intros x _,
+    simp_rw [mem_Union, mem_preimage],
+    use [y * x⁻¹, mem_univ _],
+    rwa [inv_mul_cancel_right] }
+end
+
+@[to_additive measure_theory.measure.is_add_left_invariant.null_iff]
+lemma is_mul_left_invariant.null_iff (hμ : regular μ) (h2μ : is_mul_left_invariant μ)
+  {s : set G} (hs : is_open s) : μ s = 0 ↔ s = ∅ ∨ μ = 0 :=
+begin
+  by_cases h3μ : μ = 0, { simp [h3μ] },
+  simp only [h3μ, or_false],
+  exact h2μ.null_iff_empty hμ h3μ hs,
+end
+
+@[to_additive measure_theory.measure.is_add_left_invariant.measure_ne_zero_iff_nonempty]
+lemma is_mul_left_invariant.measure_ne_zero_iff_nonempty (hμ : regular μ)
+  (h2μ : is_mul_left_invariant μ) (h3μ : μ ≠ 0) {s : set G} (hs : is_open s) :
+  μ s ≠ 0 ↔ s.nonempty :=
+by simp_rw [← ne_empty_iff_nonempty, ne.def, h2μ.null_iff_empty hμ h3μ hs]
+
+/-- For nonzero regular left invariant measures, the integral of a continuous nonnegative function
+  `f` is 0 iff `f` is 0. -/
+-- @[to_additive] (fails for now)
+lemma lintegral_eq_zero_of_is_mul_left_invariant (hμ : regular μ)
+  (h2μ : is_mul_left_invariant μ) (h3μ : μ ≠ 0) {f : G → ennreal} (hf : continuous f) :
+  ∫⁻ x, f x ∂μ = 0 ↔ f = 0 :=
+begin
+  split, swap, { rintro rfl, simp_rw [pi.zero_apply, lintegral_zero] },
+  intro h, contrapose h,
+  simp_rw [funext_iff, not_forall, pi.zero_apply] at h, cases h with x hx,
+  obtain ⟨r, h1r, h2r⟩ : ∃ r : ennreal, 0 < r ∧ r < f x :=
+  exists_between (pos_iff_ne_zero.mpr hx),
+  have h3r := hf.is_open_preimage (Ioi r) is_open_Ioi,
+  let s := Ioi r,
+  rw [← ne.def, ← pos_iff_ne_zero],
+  have : 0 < r * μ (f ⁻¹' Ioi r),
+  { rw ennreal.mul_pos,
+    refine ⟨h1r, _⟩,
+    rw [pos_iff_ne_zero, h2μ.measure_ne_zero_iff_nonempty hμ h3μ h3r],
+    exact ⟨x, h2r⟩ },
+  refine this.trans_le _,
+  rw [← set_lintegral_const, ← lintegral_indicator _ h3r.is_measurable],
+  apply lintegral_mono,
+  refine indicator_le (λ y, le_of_lt),
+end
 
-end conj
+end group
 
 end measure_theory