English
Let μ, μ′ be left-invariant measures on G. If μ and μ′ are regular, then μ′ = haarScalarFactor μ′ μ · μ.
Русский
Пусть μ и μ′ — лево-инвариантные меры на G, обе регулярны; тогда μ′ = haarScalarFactor μ′ μ · μ.
LaTeX
$$$\\forall G \\, [\\text{LocallyCompactSpace } G] \\, (μ' : \\mathrm{Measure}(G)) \\, (μ : \\mathrm{Measure}(G)) \\, [\\text{IsHaarMeasure } μ] \\, [\\text{IsFiniteMeasureOnCompacts } μ'] \\, [\\text{IsMulLeftInvariant } μ'] \\, [\\text{Regular } μ] \\, [\\text{Regular } μ'] \\, μ' = haarScalarFactor μ' μ · μ$$
Lean4
/-- **Uniqueness of left-invariant measures**:
Given two left-invariant measures which are finite
on compacts and regular, they coincide up to a multiplicative constant. -/
@[to_additive isAddLeftInvariant_eq_smul_of_regular]
theorem isMulLeftInvariant_eq_smul_of_regular [LocallyCompactSpace G] (μ' μ : Measure G) [IsHaarMeasure μ]
[IsFiniteMeasureOnCompacts μ'] [IsMulLeftInvariant μ'] [Regular μ] [Regular μ'] : μ' = haarScalarFactor μ' μ • μ :=
by
have A : ∀ U, IsOpen U → μ' U = (haarScalarFactor μ' μ • μ) U :=
by
intro U hU
rw [hU.measure_eq_iSup_isCompact, hU.measure_eq_iSup_isCompact]
congr! 4 with K _KU K_comp
exact measure_isMulLeftInvariant_eq_smul_of_ne_top μ' μ K_comp.measure_lt_top.ne K_comp.measure_lt_top.ne
ext s _hs
rw [s.measure_eq_iInf_isOpen, s.measure_eq_iInf_isOpen]
congr! 4 with U _sU U_open
exact A U U_open
