feat(measure_theory/group/prod): generalize topological groups to mea…

…surable groups (#11933)

* This fixes the gap in `[Halmos]` that I mentioned in `measure_theory.group.prod`
* Thanks to @sgouezel for giving me the proof to fill that gap.
* A text proof to fill the gap is [here](https://math.stackexchange.com/a/4387664/463377)

src/algebra/indicator_function.lean

@@ -159,6 +159,10 @@ s.apply_piecewise _ _ (λ _, h)
   mul_indicator (f ⁻¹' s) (g ∘ f) x = mul_indicator s g (f x) :=
 by { simp only [mul_indicator], split_ifs; refl }
 
+@[to_additive] lemma mul_indicator_image {s : set α} {f : β → M} {g : α → β} (hg : injective g)
+  {x : α} : mul_indicator (g '' s) f (g x) = mul_indicator s (f ∘ g) x :=
+by rw [← mul_indicator_comp_right, preimage_image_eq _ hg]
+
 @[to_additive] lemma mul_indicator_comp_of_one {g : M → N} (hg : g 1 = 1) :
   mul_indicator s (g ∘ f) = g ∘ (mul_indicator s f) :=
 begin

src/measure_theory/group/measure.lean

@@ -143,8 +143,13 @@ lemma inv_apply (μ : measure G) (s : set G) : μ.inv s = μ s⁻¹ :=
 end measure
 
 section inv
-variables [group G] [has_measurable_mul G] [has_measurable_inv G]
-  {μ : measure G}
+variables [group G] [has_measurable_inv G] {μ : measure G}
+
+@[to_additive]
+instance [sigma_finite μ] : sigma_finite μ.inv :=
+(measurable_equiv.inv G).sigma_finite_map ‹_›
+
+variables [has_measurable_mul G]
 
 @[to_additive]
 instance [is_mul_left_invariant μ] : is_mul_right_invariant μ.inv :=

src/measure_theory/group/prod.lean

@@ -8,11 +8,10 @@ import measure_theory.group.measure
 
 /-!
 # Measure theory in the product of groups
+In this file we show properties about measure theory in products of measurable groups
+and properties of iterated integrals in measurable groups.
 
-In this file we show properties about measure theory in products of topological groups
-and properties of iterated integrals in topological groups.
-
-These lemmas show the uniqueness of left invariant measures on locally compact groups, up to
+These lemmas show the uniqueness of left invariant measures on measurable groups, up to
 scaling. In this file we follow the proof and refer to the book *Measure Theory* by Paul Halmos.
 
 The idea of the proof is to use the translation invariance of measures to prove `μ(F) = c * μ(E)`
@@ -29,27 +28,32 @@ Applying this to `μ` and to `ν` gives `μ (F) / μ (E) = ν (F) / ν (E)`, whi
 scalar multiplication.
 
 The proof in [Halmos] seems to contain an omission in §60 Th. A, see
-`measure_theory.measure_lintegral_div_measure` and
-https://math.stackexchange.com/questions/3974485/does-right-translation-preserve-finiteness-for-a-left-invariant-measure
-
-## Todo
+`measure_theory.measure_lintegral_div_measure`.
 
-Much of the results in this file work in a group with measurable multiplication instead of a
-topological group
 -/
 
 noncomputable theory
-open topological_space set (hiding prod_eq) function
-open_locale classical ennreal pointwise
+open set (hiding prod_eq) function measure_theory
+open_locale classical ennreal pointwise measure_theory
+
+variables (G : Type*) [measurable_space G]
+variables [group G] [has_measurable_mul₂ G]
+variables (μ ν : measure G) [sigma_finite ν] [sigma_finite μ]
+
+/-- The map `(x, y) ↦ (x, xy)` as a `measurable_equiv`. This is a shear mapping. -/
+@[to_additive "The map `(x, y) ↦ (x, x + y)` as a `measurable_equiv`.
+This is a shear mapping."]
+protected def measurable_equiv.shear_mul_right [has_measurable_inv G] : G × G ≃ᵐ G × G :=
+{ measurable_to_fun  := measurable_fst.prod_mk measurable_mul,
+  measurable_inv_fun := measurable_fst.prod_mk $ measurable_fst.inv.mul measurable_snd,
+  .. equiv.prod_shear (equiv.refl _) equiv.mul_left }
+
+variables {G}
 
 namespace measure_theory
 
 open measure
 
-variables {G : Type*} [topological_space G] [measurable_space G] [second_countable_topology G]
-variables [borel_space G] [group G] [topological_group G]
-variables (μ ν : measure G) [sigma_finite ν] [sigma_finite μ]
-
 /-- This condition is part of the definition of a measurable group in [Halmos, §59].
   There, the map in this lemma is called `S`. -/
 @[to_additive map_prod_sum_eq]
@@ -75,13 +79,25 @@ begin
   exact map_prod_mul_eq ν μ
 end
 
+@[to_additive]
+lemma measurable_measure_mul_right {E : set G} (hE : measurable_set E) :
+  measurable (λ x, μ ((λ y, y * x) ⁻¹' E)) :=
+begin
+  suffices : measurable (λ y,
+    μ ((λ x, (x, y)) ⁻¹' ((λ z : G × G, ((1 : G), z.1 * z.2)) ⁻¹' ((univ : set G) ×ˢ E)))),
+  { convert this, ext1 x, congr' 1 with y : 1, simp },
+  apply measurable_measure_prod_mk_right,
+  exact measurable_const.prod_mk (measurable_fst.mul measurable_snd) (measurable_set.univ.prod hE)
+end
+
+variables [has_measurable_inv G]
+
 /-- The function we are mapping along is `S⁻¹` in [Halmos, §59],
   where `S` is the map in `map_prod_mul_eq`. -/
 @[to_additive map_prod_neg_add_eq]
 lemma map_prod_inv_mul_eq [is_mul_left_invariant ν] :
   map (λ z : G × G, (z.1, z.1⁻¹ * z.2)) (μ.prod ν) = μ.prod ν :=
-(homeomorph.shear_mul_right G).to_measurable_equiv.map_apply_eq_iff_map_symm_apply_eq.mp $
-  map_prod_mul_eq μ ν
+(measurable_equiv.shear_mul_right G).map_apply_eq_iff_map_symm_apply_eq.mp $ map_prod_mul_eq μ ν
 
 /-- The function we are mapping along is `S⁻¹R` in [Halmos, §59],
   where `S` is the map in `map_prod_mul_eq` and `R` is `prod.swap`. -/
@@ -101,7 +117,6 @@ end
 lemma map_prod_mul_inv_eq [is_mul_left_invariant μ] [is_mul_left_invariant ν] :
   map (λ z : G × G, (z.2 * z.1, z.1⁻¹)) (μ.prod ν) = μ.prod ν :=
 begin
-  let S := (homeomorph.shear_mul_right G).to_measurable_equiv,
   suffices : map ((λ z : G × G, (z.2, z.2⁻¹ * z.1)) ∘ (λ z : G × G, (z.2, z.2 * z.1))) (μ.prod ν) =
     μ.prod ν,
   { convert this, ext1 ⟨x, y⟩, simp },
@@ -133,17 +148,6 @@ begin
   exact (inv_inv _).symm
 end
 
-@[to_additive]
-lemma measurable_measure_mul_right {E : set G} (hE : measurable_set E) :
-  measurable (λ x, μ ((λ y, y * x) ⁻¹' E)) :=
-begin
-  suffices : measurable (λ y,
-    μ ((λ x, (x, y)) ⁻¹' ((λ z : G × G, ((1 : G), z.1 * z.2)) ⁻¹' ((univ : set G) ×ˢ E)))),
-  { convert this, ext1 x, congr' 1 with y : 1, simp },
-  apply measurable_measure_prod_mk_right,
-  exact measurable_const.prod_mk (measurable_fst.mul measurable_snd) (measurable_set.univ.prod hE)
-end
-
 @[to_additive]
 lemma lintegral_lintegral_mul_inv [is_mul_left_invariant μ] [is_mul_left_invariant ν]
   (f : G → G → ℝ≥0∞) (hf : ae_measurable (uncurry f) (μ.prod ν)) :
@@ -171,57 +175,115 @@ lemma measure_mul_right_ne_zero [is_mul_left_invariant μ] {E : set G}
   (h2E : μ E ≠ 0) (y : G) : μ ((λ x, x * y) ⁻¹' E) ≠ 0 :=
 (not_iff_not_of_iff (measure_mul_right_null μ y)).mpr h2E
 
-/-- A technical lemma relating two different measures. This is basically [Halmos, §60 Th. A].
-  Note that if `f` is the characteristic function of a measurable set `F` this states that
-  `μ F = c * μ E` for a constant `c` that does not depend on `μ`.
-  There seems to be a gap in the last step of the proof in [Halmos].
-  In the last line, the equality `g(x⁻¹)ν(Ex⁻¹) = f(x)` holds if we can prove that
-  `0 < ν(Ex⁻¹) < ∞`. The first inequality follows from §59, Th. D, but I couldn't find the second
-  inequality. For this reason, we use a compact `E` instead of a measurable `E` as in [Halmos], and
-  additionally assume that `ν` is a regular measure (we only need that it is finite on compact
-  sets). -/
+/-- This is the computation performed in the proof of [Halmos, §60 Th. A]. -/
 @[to_additive]
-lemma measure_lintegral_div_measure [t2_space G] [is_mul_left_invariant μ]
-  [is_mul_left_invariant ν] [regular ν] {E : set G} (hE : is_compact E) (h2E : ν E ≠ 0)
-  (f : G → ℝ≥0∞) (hf : measurable f) :
-  μ E * ∫⁻ y, f y⁻¹ / ν ((λ h, h * y⁻¹) ⁻¹' E) ∂ν = ∫⁻ x, f x ∂μ :=
+lemma measure_mul_lintegral_eq [is_mul_left_invariant μ]
+  [is_mul_left_invariant ν] {E : set G} (Em : measurable_set E) (f : G → ℝ≥0∞) (hf : measurable f) :
+  μ E * ∫⁻ y, f y ∂ν = ∫⁻ x, ν ((λ z, z * x) ⁻¹' E) * f (x⁻¹) ∂μ :=
 begin
-  have Em := hE.measurable_set,
-  symmetry,
-  set g := λ y, f y⁻¹ / ν ((λ h, h * y⁻¹) ⁻¹' E),
-  have hg : measurable g := (hf.comp measurable_inv).div
-    ((measurable_measure_mul_right ν Em).comp measurable_inv),
   rw [← set_lintegral_one, ← lintegral_indicator _ Em,
-    ← lintegral_lintegral_mul (measurable_const.indicator Em).ae_measurable hg.ae_measurable,
+    ← lintegral_lintegral_mul (measurable_const.indicator Em).ae_measurable hf.ae_measurable,
     ← lintegral_lintegral_mul_inv μ ν],
   swap, { exact (((measurable_const.indicator Em).comp measurable_fst).mul
-      (hg.comp measurable_snd)).ae_measurable },
+      (hf.comp measurable_snd)).ae_measurable },
   have mE : ∀ x : G, measurable (λ y, ((λ z, z * x) ⁻¹' E).indicator (λ z, (1 : ℝ≥0∞)) y) :=
   λ x, measurable_const.indicator (measurable_mul_const _ Em),
   have : ∀ x y, E.indicator (λ (z : G), (1 : ℝ≥0∞)) (y * x) =
     ((λ z, z * x) ⁻¹' E).indicator (λ (b : G), 1) y,
   { intros x y, symmetry, convert indicator_comp_right (λ y, y * x), ext1 z, refl },
-  have h3E : ∀ y, ν ((λ x, x * y) ⁻¹' E) ≠ ∞ :=
-    λ y, (is_compact.measure_lt_top $ (homeomorph.mul_right _).compact_preimage.mpr hE).ne,
   simp_rw [this, lintegral_mul_const _ (mE _), lintegral_indicator _ (measurable_mul_const _ Em),
-    set_lintegral_one, g, inv_inv,
-    ennreal.mul_div_cancel' (measure_mul_right_ne_zero ν h2E _) (h3E _)]
+    set_lintegral_one],
+end
+
+/-- Any two nonzero left-invariant measures are absolutely continuous w.r.t. each other. -/
+@[to_additive]
+lemma absolutely_continuous_of_is_mul_left_invariant
+  [is_mul_left_invariant μ] [is_mul_left_invariant ν] (hν : ν ≠ 0) : μ ≪ ν :=
+begin
+  refine absolutely_continuous.mk (λ E Em hνE, _),
+  have h1 := measure_mul_lintegral_eq μ ν Em 1 measurable_one,
+  simp_rw [pi.one_apply, lintegral_one, mul_one, (measure_mul_right_null ν _).mpr hνE,
+    lintegral_zero, mul_eq_zero, measure_univ_eq_zero.not.mpr hν, or_false] at h1,
+  exact h1
 end
 
-/-- This is roughly the uniqueness (up to a scalar) of left invariant Borel measures on a second
-  countable locally compact group. The uniqueness of Haar measure is proven from this in
-  `measure_theory.measure.haar_measure_unique` -/
 @[to_additive]
-lemma measure_mul_measure_eq [t2_space G] [is_mul_left_invariant μ]
-  [is_mul_left_invariant ν] [regular ν] {E F : set G}
-  (hE : is_compact E) (hF : measurable_set F) (h2E : ν E ≠ 0) : μ E * ν F = ν E * μ F :=
+lemma ae_measure_preimage_mul_right_lt_top [is_mul_left_invariant μ] [is_mul_left_invariant ν]
+  {E : set G} (Em : measurable_set E) (hμE : μ E ≠ ∞) :
+  ∀ᵐ x ∂μ, ν ((λ y, y * x) ⁻¹' E) < ∞ :=
 begin
-  have h1 := measure_lintegral_div_measure ν ν hE h2E (F.indicator (λ x, 1))
+  refine ae_of_forall_measure_lt_top_ae_restrict' ν.inv _ _,
+  intros A hA h2A h3A,
+  simp only [ν.inv_apply] at h3A,
+  apply ae_lt_top (measurable_measure_mul_right ν Em),
+  have h1 := measure_mul_lintegral_eq μ ν Em (A⁻¹.indicator 1) (measurable_one.indicator hA.inv),
+  rw [lintegral_indicator _ hA.inv] at h1,
+  simp_rw [pi.one_apply, set_lintegral_one, ← image_inv, indicator_image inv_injective, image_inv,
+    ← indicator_mul_right _ (λ x, ν ((λ y, y * x) ⁻¹' E)), function.comp, pi.one_apply,
+    mul_one] at h1,
+  rw [← lintegral_indicator _ hA, ← h1],
+  exact ennreal.mul_ne_top hμE h3A.ne,
+end
+
+@[to_additive]
+lemma ae_measure_preimage_mul_right_lt_top_of_ne_zero [is_mul_left_invariant μ]
+  [is_mul_left_invariant ν] {E : set G} (Em : measurable_set E) (h2E : ν E ≠ 0) (h3E : ν E ≠ ∞) :
+  ∀ᵐ x ∂μ, ν ((λ y, y * x) ⁻¹' E) < ∞ :=
+begin
+  refine (ae_measure_preimage_mul_right_lt_top ν ν Em h3E).filter_mono _,
+  refine (absolutely_continuous_of_is_mul_left_invariant μ ν _).ae_le,
+  refine mt _ h2E,
+  intro hν,
+  rw [hν, measure.coe_zero, pi.zero_apply]
+end
+
+/-- A technical lemma relating two different measures. This is basically [Halmos, §60 Th. A].
+  Note that if `f` is the characteristic function of a measurable set `F` this states that
+  `μ F = c * μ E` for a constant `c` that does not depend on `μ`.
+
+  Note: There is a gap in the last step of the proof in [Halmos].
+  In the last line, the equality `g(x⁻¹)ν(Ex⁻¹) = f(x)` holds if we can prove that
+  `0 < ν(Ex⁻¹) < ∞`. The first inequality follows from §59, Th. D, but the second inequality is
+  not justified. We prove this inequality for almost all `x` in
+  `measure_theory.ae_measure_preimage_mul_right_lt_top_of_ne_zero`. -/
+@[to_additive]
+lemma measure_lintegral_div_measure [is_mul_left_invariant μ]
+  [is_mul_left_invariant ν] {E : set G} (Em : measurable_set E) (h2E : ν E ≠ 0) (h3E : ν E ≠ ∞)
+  (f : G → ℝ≥0∞) (hf : measurable f) :
+  μ E * ∫⁻ y, f y⁻¹ / ν ((λ x, x * y⁻¹) ⁻¹' E) ∂ν = ∫⁻ x, f x ∂μ :=
+begin
+  set g := λ y, f y⁻¹ / ν ((λ x, x * y⁻¹) ⁻¹' E),
+  have hg : measurable g := (hf.comp measurable_inv).div
+    ((measurable_measure_mul_right ν Em).comp measurable_inv),
+  simp_rw [measure_mul_lintegral_eq μ ν Em g hg, g, inv_inv],
+  refine lintegral_congr_ae _,
+  refine (ae_measure_preimage_mul_right_lt_top_of_ne_zero μ ν Em h2E h3E).mono (λ x hx , _),
+  simp_rw [ennreal.mul_div_cancel' (measure_mul_right_ne_zero ν h2E _) hx.ne]
+end
+
+@[to_additive]
+lemma measure_mul_measure_eq [is_mul_left_invariant μ]
+  [is_mul_left_invariant ν] {E F : set G}
+  (hE : measurable_set E) (hF : measurable_set F) (h2E : ν E ≠ 0) (h3E : ν E ≠ ∞) :
+    μ E * ν F = ν E * μ F :=
+begin
+  have h1 := measure_lintegral_div_measure ν ν hE h2E h3E (F.indicator (λ x, 1))
     (measurable_const.indicator hF),
-  have h2 := measure_lintegral_div_measure μ ν hE h2E (F.indicator (λ x, 1))
+  have h2 := measure_lintegral_div_measure μ ν hE h2E h3E (F.indicator (λ x, 1))
     (measurable_const.indicator hF),
   rw [lintegral_indicator _ hF, set_lintegral_one] at h1 h2,
   rw [← h1, mul_left_comm, h2],
 end
 
+/-- Left invariant Borel measures on a measurable group are unique (up to a scalar). -/
+@[to_additive]
+lemma measure_eq_div_smul [is_mul_left_invariant μ]
+  [is_mul_left_invariant ν] {E : set G}
+  (hE : measurable_set E) (h2E : ν E ≠ 0) (h3E : ν E ≠ ∞) : μ = (μ E / ν E) • ν :=
+begin
+  ext1 F hF,
+  rw [smul_apply, smul_eq_mul, mul_comm, ← mul_div_assoc, mul_comm,
+    measure_mul_measure_eq μ ν hE hF h2E h3E, mul_div_assoc, ennreal.mul_div_cancel' h2E h3E]
+end
+
 end measure_theory

src/measure_theory/measure/haar.lean

@@ -578,54 +578,59 @@ end
 additive group."]
 def haar [locally_compact_space G] : measure G := haar_measure $ classical.arbitrary _
 
-section unique
+section second_countable
 
 variables [second_countable_topology G]
 
 /-- The Haar measure is unique up to scaling. More precisely: every σ-finite left invariant measure
-  is a scalar multiple of the Haar measure. -/
+  is a scalar multiple of the Haar measure.
+  This is slightly weaker than assuming that `μ` is a Haar measure (in particular we don't require
+  `μ ≠ 0`). -/
 @[to_additive]
 theorem haar_measure_unique (μ : measure G) [sigma_finite μ] [is_mul_left_invariant μ]
   (K₀ : positive_compacts G) : μ = μ K₀ • haar_measure K₀ :=
 begin
-  ext1 s hs,
-  have := measure_mul_measure_eq μ (haar_measure K₀) K₀.compact hs,
-  rw [haar_measure_self, one_mul] at this,
-  rw [← this (by norm_num), smul_apply, smul_eq_mul],
+  refine (measure_eq_div_smul μ (haar_measure K₀) K₀.compact.measurable_set
+    (measure_pos_of_nonempty_interior _ K₀.interior_nonempty).ne'
+    K₀.compact.measure_lt_top.ne).trans _,
+  rw [haar_measure_self, ennreal.div_one]
 end
 
+example [locally_compact_space G] (μ : measure G) [is_haar_measure μ] (K₀ : positive_compacts G) :
+  μ = μ K₀.1 • haar_measure K₀ :=
+haar_measure_unique μ K₀
+
+/-- To show that an invariant σ-finite measure is regular it is sufficient to show that it is finite
+  on some compact set with non-empty interior. -/
 @[to_additive]
 theorem regular_of_is_mul_left_invariant {μ : measure G} [sigma_finite μ] [is_mul_left_invariant μ]
   {K : set G} (hK : is_compact K) (h2K : (interior K).nonempty) (hμK : μ K ≠ ∞) :
   regular μ :=
 by { rw [haar_measure_unique μ ⟨⟨K, hK⟩, h2K⟩], exact regular.smul hμK }
 
-end unique
-
 @[to_additive is_add_haar_measure_eq_smul_is_add_haar_measure]
 theorem is_haar_measure_eq_smul_is_haar_measure
-  [locally_compact_space G] [second_countable_topology G]
-  (μ ν : measure G) [is_haar_measure μ] [is_haar_measure ν] :
-  ∃ (c : ℝ≥0∞), (c ≠ 0) ∧ (c ≠ ∞) ∧ (μ = c • ν) :=
+  [locally_compact_space G] (μ ν : measure G) [is_haar_measure μ] [is_haar_measure ν] :
+  ∃ (c : ℝ≥0∞), c ≠ 0 ∧ c ≠ ∞ ∧ μ = c • ν :=
 begin
   have K : positive_compacts G := classical.arbitrary _,
   have νpos : 0 < ν K := measure_pos_of_nonempty_interior _ K.interior_nonempty,
-  have νlt : ν K < ∞ := K.compact.measure_lt_top ,
+  have νne : ν K ≠ ∞ := K.compact.measure_lt_top.ne,
   refine ⟨μ K / ν K, _, _, _⟩,
-  { simp only [νlt.ne, (μ.measure_pos_of_nonempty_interior K.interior_nonempty).ne', ne.def,
+  { simp only [νne, (μ.measure_pos_of_nonempty_interior K.interior_nonempty).ne', ne.def,
       ennreal.div_zero_iff, not_false_iff, or_self] },
-  { simp only [div_eq_mul_inv, νpos.ne', K.compact.measure_lt_top.ne, or_self,
+  { simp only [div_eq_mul_inv, νpos.ne', (K.compact.measure_lt_top).ne, or_self,
       ennreal.inv_eq_top, with_top.mul_eq_top_iff, ne.def, not_false_iff, and_false, false_and] },
   { calc
     μ = μ K • haar_measure K : haar_measure_unique μ K
     ... = (μ K / ν K) • (ν K • haar_measure K) :
-      by rw [smul_smul, div_eq_mul_inv, mul_assoc, ennreal.inv_mul_cancel νpos.ne' νlt.ne, mul_one]
+      by rw [smul_smul, div_eq_mul_inv, mul_assoc, ennreal.inv_mul_cancel νpos.ne' νne, mul_one]
     ... = (μ K / ν K) • ν : by rw ← haar_measure_unique ν K }
 end
 
-@[priority 90, to_additive] -- see Note [lower instance priority]]
+@[priority 90, to_additive] -- see Note [lower instance priority]
 instance regular_of_is_haar_measure
-  [locally_compact_space G] [second_countable_topology G] (μ : measure G) [is_haar_measure μ] :
+  [locally_compact_space G] (μ : measure G) [is_haar_measure μ] :
   regular μ :=
 begin
   have K : positive_compacts G := classical.arbitrary _,
@@ -635,6 +640,8 @@ begin
   exact regular.smul ctop,
 end
 
+end second_countable
+
 /-- Any Haar measure is invariant under inversion in a commutative group. -/
 @[to_additive]
 lemma map_haar_inv