English
Let G be a locally compact group. If μ and μ′ are Haar probability measures on G, then μ′ = μ.
Русский
Пусть G — локально компактная группа. Пусть μ и μ′ — меры Хаара на G, нормированные так, чтобы μ(G) = μ′(G) = 1. Тогда μ′ = μ.
LaTeX
$$$\\forall G \\, [\\text{LocallyCompactSpace } G] \\, (μ' : \\mathrm{Measure}(G)) \\, (μ : \\mathrm{Measure}(G)) \\, [\\text{IsHaarMeasure } μ] \\, [\\text{IsHaarMeasure } μ'] \Rightarrow μ' = μ$$
Lean4
/-- **Uniqueness of Haar measures**:
Two Haar measures which are probability measures coincide. -/
@[to_additive]
theorem isHaarMeasure_eq_of_isProbabilityMeasure [LocallyCompactSpace G] (μ' μ : Measure G) [IsProbabilityMeasure μ]
[IsProbabilityMeasure μ'] [IsHaarMeasure μ] [IsHaarMeasure μ'] : μ' = μ :=
by
have : CompactSpace G := by
by_contra H
rw [not_compactSpace_iff] at H
simpa using measure_univ_of_isMulLeftInvariant μ
have A s : μ' s = haarScalarFactor μ' μ • μ s :=
measure_isMulInvariant_eq_smul_of_isCompact_closure _ _ isClosed_closure.isCompact
have Z := A univ
simp only [measure_univ, ENNReal.smul_def, smul_eq_mul, mul_one, ENNReal.one_eq_coe] at Z
ext s _hs
simp [A s, ← Z]
