feat(haar_measure): define the Haar measure (#3542)

Define the Haar measure on a locally compact Hausdorff group.
Some additions and simplifications to outer_measure and content.



Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

Author: fpvandoorn

docs/references.bib

@@ -317,4 +317,13 @@ @inproceedings{fuerer-lochbihler-schneider-traytel2020
   timestamp = {Mon, 06 Jul 2020 09:05:32 +0200},
   biburl    = {https://dblp.org/rec/conf/cade/FurerLST20.bib},
   bibsource = {dblp computer science bibliography, https://dblp.org}
-}
+}
+
+@book{halmos1950measure,
+  author    = {Halmos, Paul R},
+  title     = {Measure theory},
+  publisher = {Springer-Verlag New York},
+  year      = 1950,
+  isbn      = {978-1-4684-9440-2},
+  doi       = {10.1007/978-1-4684-9440-2}
+}

src/measure_theory/content.lean

@@ -129,16 +129,21 @@ lemma inner_content_Union_nat [t2_space G] {μ : compacts G → ennreal}
   inner_content μ ⟨⋃ (i : ℕ), U i, is_open_Union hU⟩ ≤ ∑' (i : ℕ), inner_content μ ⟨U i, hU i⟩ :=
 by { have := inner_content_Sup_nat h1 h2 (λ i, ⟨U i, hU i⟩), rwa [opens.supr_def] at this }
 
-lemma is_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 :=
+lemma inner_content_comap {μ : compacts G → ennreal} (f : G ≃ₜ G)
+  (h : ∀ ⦃K : compacts G⦄, μ (K.map f f.continuous) = μ K) (U : opens G) :
+  inner_content μ (U.comap f.continuous) = inner_content μ U :=
 begin
-  refine supr_congr _ ((compacts.equiv (homeomorph.mul_left g)).surjective) _,
+  refine supr_congr _ ((compacts.equiv f).surjective) _,
   intro K, refine supr_congr_Prop image_subset_iff _,
   intro hK, simp only [equiv.coe_fn_mk, subtype.mk_eq_mk, ennreal.coe_eq_coe, compacts.equiv],
-  apply h
+  apply h,
 end
 
+lemma is_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}
   (h1 : μ ⊥ = 0)
   (h2 : ∀ (K₁ K₂ : compacts G), μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂)
@@ -185,6 +190,10 @@ begin
   { exact inner_content_mono }
 end
 
+lemma of_content_eq_infi (A : set G) :
+  of_content μ h1 A = ⨅ (U : set G) (hU : is_open U) (h : A ⊆ U), inner_content μ ⟨U, hU⟩ :=
+induced_outer_measure_eq_infi _ (inner_content_Union_nat h1 h2) inner_content_mono A
+
 lemma of_content_interior_compacts (h3 : ∀ (K₁ K₂ : compacts G), K₁.1 ⊆ K₂.1 → μ K₁ ≤ μ K₂)
   (K : compacts G) : of_content μ h1 (interior K.1) ≤ μ K :=
 le_trans (le_of_eq $ of_content_opens h2 (opens.interior K.1))
@@ -205,6 +214,29 @@ begin
   exact ⟨⟨U, hU⟩, h2U, h3U⟩, swap, exact inner_content_Union_nat h1 h2
 end
 
+lemma of_content_preimage (f : G ≃ₜ G) (h : ∀ ⦃K : compacts G⦄, μ (K.map f f.continuous) = μ K)
+  (A : set G) : of_content μ h1 (f ⁻¹' A) = of_content μ h1 A :=
+begin
+  refine induced_outer_measure_preimage _ (inner_content_Union_nat h1 h2) inner_content_mono _
+    (λ s, f.is_open_preimage) _,
+  intros s hs, convert inner_content_comap f h ⟨s, hs⟩
+end
+
+lemma is_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
+
+lemma of_content_caratheodory (A : set G) :
+  (of_content μ h1).caratheodory.is_measurable A ↔ ∀ (U : opens G),
+  of_content μ h1 (U ∩ A) + of_content μ h1 (U \ A) ≤ of_content μ h1 U :=
+begin
+  dsimp [opens], rw subtype.forall,
+  apply induced_outer_measure_caratheodory,
+  apply inner_content_Union_nat h1 h2,
+  apply inner_content_mono'
+end
+
 lemma of_content_pos_of_is_open [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) :