feat: uniqueness of Haar measure in general locally compact groups (#…

…8198)

We prove that two regular Haar measures in a locally compact group coincide up to scalar multiplication, and the same thing for inner regular Haar measures. This is implemented in a new file `MeasureTheory.Measure.Haar.Unique`. A few results that used to be in the `MeasureTheory.Measure.Haar.Basic` are moved to this file (and extended) so several imports have to be changed.

Mathlib.lean

@@ -2606,6 +2606,7 @@ import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
 import Mathlib.MeasureTheory.Measure.Haar.NormedSpace
 import Mathlib.MeasureTheory.Measure.Haar.OfBasis
 import Mathlib.MeasureTheory.Measure.Haar.Quotient
+import Mathlib.MeasureTheory.Measure.Haar.Unique
 import Mathlib.MeasureTheory.Measure.Hausdorff
 import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
 import Mathlib.MeasureTheory.Measure.Lebesgue.Complex

Mathlib/Analysis/Calculus/BumpFunction/Convolution.lean

@@ -8,6 +8,7 @@ import Mathlib.Analysis.Calculus.BumpFunction.Normed
 import Mathlib.MeasureTheory.Integral.Average
 import Mathlib.MeasureTheory.Covering.Differentiation
 import Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
+import Mathlib.MeasureTheory.Measure.Haar.Unique
 
 #align_import analysis.convolution from "leanprover-community/mathlib"@"8905e5ed90859939681a725b00f6063e65096d95"
 

Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean

@@ -11,6 +11,7 @@ import Mathlib.MeasureTheory.Group.Integral
 import Mathlib.MeasureTheory.Integral.SetIntegral
 import Mathlib.MeasureTheory.Measure.Haar.NormedSpace
 import Mathlib.Topology.EMetricSpace.Paracompact
+import Mathlib.MeasureTheory.Measure.Haar.Unique
 
 #align_import analysis.fourier.riemann_lebesgue_lemma from "leanprover-community/mathlib"@"fd5edc43dc4f10b85abfe544b88f82cf13c5f844"
 
@@ -259,7 +260,7 @@ via dual space. **Do not use** -- it is only a stepping stone to
 `tendsto_integral_exp_smul_cocompact` where the inner-product-space structure isn't required. -/
 theorem tendsto_integral_exp_smul_cocompact_of_inner_product (μ : Measure V) [μ.IsAddHaarMeasure] :
     Tendsto (fun w : V →L[ℝ] ℝ => ∫ v, e[-w v] • f v ∂μ) (cocompact (V →L[ℝ] ℝ)) (𝓝 0) := by
-  obtain ⟨C, _, _, hC⟩ := μ.isAddHaarMeasure_eq_smul_isAddHaarMeasure volume
+  obtain ⟨C, _, _, hC⟩ := μ.isAddHaarMeasure_eq_smul volume
   rw [hC]
   simp_rw [integral_smul_measure]
   rw [← (smul_zero _ : C.toReal • (0 : E) = 0)]

Mathlib/Dynamics/Ergodic/AddCircle.lean

@@ -7,6 +7,7 @@ import Mathlib.MeasureTheory.Group.AddCircle
 import Mathlib.Dynamics.Ergodic.Ergodic
 import Mathlib.MeasureTheory.Covering.DensityTheorem
 import Mathlib.Data.Set.Pointwise.Iterate
+import Mathlib.MeasureTheory.Measure.Haar.Unique
 
 #align_import dynamics.ergodic.add_circle from "leanprover-community/mathlib"@"5f6e827d81dfbeb6151d7016586ceeb0099b9655"
 

Mathlib/MeasureTheory/Group/Measure.lean

@@ -548,6 +548,16 @@ section TopologicalGroup
 
 variable [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [Group G]
 
+@[to_additive]
+instance Measure.IsFiniteMeasureOnCompacts.inv [ContinuousInv G] [IsFiniteMeasureOnCompacts μ] :
+    IsFiniteMeasureOnCompacts μ.inv :=
+  IsFiniteMeasureOnCompacts.map μ (Homeomorph.inv G)
+
+@[to_additive]
+instance Measure.IsOpenPosMeasure.inv [ContinuousInv G] [IsOpenPosMeasure μ] :
+    IsOpenPosMeasure μ.inv :=
+  (Homeomorph.inv G).continuous.isOpenPosMeasure_map (Homeomorph.inv G).surjective
+
 @[to_additive]
 instance Measure.Regular.inv [ContinuousInv G] [Regular μ] : Regular μ.inv :=
   Regular.map (Homeomorph.inv G)
@@ -561,10 +571,8 @@ instance Measure.InnerRegular.inv [ContinuousInv G] [InnerRegular μ] : InnerReg
 variable [TopologicalGroup G]
 
 @[to_additive]
-theorem regular_inv_iff : μ.inv.Regular ↔ μ.Regular := by
-  constructor
-  · intro h; rw [← μ.inv_inv]; exact Measure.Regular.inv
-  · intro h; exact Measure.Regular.inv
+theorem regular_inv_iff : μ.inv.Regular ↔ μ.Regular :=
+  Regular.map_iff (Homeomorph.inv G)
 #align measure_theory.regular_inv_iff MeasureTheory.regular_inv_iff
 #align measure_theory.regular_neg_iff MeasureTheory.regular_neg_iff
 

Mathlib/MeasureTheory/Group/Prod.lean

@@ -32,6 +32,11 @@ scalar multiplication.
 The proof in [Halmos] seems to contain an omission in §60 Th. A, see
 `MeasureTheory.measure_lintegral_div_measure`.
 
+Note that this theory only applies in measurable groups, i.e., when multiplication and inversion
+are measurable. This is not the case in general in locally compact groups, or even in compact
+groups, when the topology is not second-countable. For arguments along the same line, but using
+continuous functions instead of measurable sets and working in the general locally compact
+setting, see the file `MeasureTheory.Measure.Haar.Unique.lean`.
 -/
 
 

Mathlib/MeasureTheory/Measure/Haar/Disintegration.lean

@@ -5,6 +5,7 @@ Authors: Sébastien Gouëzel
 -/
 import Mathlib.MeasureTheory.Measure.Haar.Basic
 import Mathlib.Analysis.NormedSpace.FiniteDimension
+import Mathlib.MeasureTheory.Measure.Haar.Unique
 
 /-!
 # Pushing a Haar measure by a linear map
@@ -85,12 +86,12 @@ theorem LinearMap.exists_map_addHaar_eq_smul_addHaar' (h : Function.Surjective L
       ∃ c₀ : ℝ≥0∞, c₀ ≠ 0 ∧ c₀ ≠ ∞ ∧ μ.map M.symm = c₀ • μS.prod μT := by
     have : IsAddHaarMeasure (μ.map M.symm) :=
       M.toContinuousLinearEquiv.symm.isAddHaarMeasure_map μ
-    exact isAddHaarMeasure_eq_smul_isAddHaarMeasure _ _
+    exact isAddHaarMeasure_eq_smul _ _
   have J : (μS.prod μT).map P = (μS univ) • μT := map_snd_prod
   obtain ⟨c₁, c₁_pos, c₁_fin, h₁⟩ : ∃ c₁ : ℝ≥0∞, c₁ ≠ 0 ∧ c₁ ≠ ∞ ∧ μT.map L' = c₁ • ν := by
     have : IsAddHaarMeasure (μT.map L') :=
       L'.toContinuousLinearEquiv.isAddHaarMeasure_map μT
-    exact isAddHaarMeasure_eq_smul_isAddHaarMeasure _ _
+    exact isAddHaarMeasure_eq_smul _ _
   refine ⟨c₀ * c₁, by simp [pos_iff_ne_zero, c₀_pos, c₁_pos], ENNReal.mul_lt_top c₀_fin c₁_fin, ?_⟩
   simp only [I, h₀, Measure.map_smul, J, smul_smul, h₁]
   rw [mul_assoc, mul_comm _ c₁, ← mul_assoc]