English
Let μ, μ′ be left-invariant Haar-type measures on G. If μ and μ′ are inner regular with respect to compacts, then μ′ = haarScalarFactor μ′ μ · μ.
Русский
Пусть μ и μ′ — лево-инвариантные меры на G, подобные Хаару, и обе внутренне регулярны по компактам. Тогда μ′ = haarScalarFactor μ′ μ · μ.
LaTeX
$$$\\forall G \\, [\\text{LocallyCompactSpace } G] \\, (μ' : \\mathrm{Measure}(G)) \\, (μ : \\mathrm{Measure}(G)) \\, [\\text{IsHaarMeasure } μ] \\, [\\text{IsFiniteMeasureOnCompacts } μ'] \\, [\\text{IsMulLeftInvariant } μ'] \\, [\\text{InnerRegular } μ] \\, [\\text{InnerRegular } μ'] \\, μ' = haarScalarFactor μ' μ · μ$$
Lean4
/-- **Uniqueness of left-invariant measures**:
Given two left-invariant measures which are finite
on compacts and inner regular, they coincide up to a multiplicative constant. -/
@[to_additive isAddLeftInvariant_eq_smul_of_innerRegular]
theorem isMulLeftInvariant_eq_smul_of_innerRegular [LocallyCompactSpace G] (μ' μ : Measure G) [IsHaarMeasure μ]
[IsFiniteMeasureOnCompacts μ'] [IsMulLeftInvariant μ'] [InnerRegular μ] [InnerRegular μ'] :
μ' = haarScalarFactor μ' μ • μ := by
ext s hs
rw [hs.measure_eq_iSup_isCompact, hs.measure_eq_iSup_isCompact]
congr! 4 with K _Ks K_comp
exact measure_isMulLeftInvariant_eq_smul_of_ne_top μ' μ K_comp.measure_lt_top.ne K_comp.measure_lt_top.ne
