English
Two Haar measures on a locally compact group coincide on sets with compact closure up to the Haar-scalar factor.
Русский
Две меры Хаара на локально компактной группе совпадают на множествах с компактным замыканием до коэффициента Хаара.
LaTeX
$$$$ μ'\\, s = haarScalarFactor μ' μ \\cdot μ s, \\quad \\text{for } s \\text{ with } closure(s) \\text{ compact}.$$$$
Lean4
@[to_additive (attr := simp)]
theorem haarScalarFactor_self (μ : Measure G) [IsHaarMeasure μ] : haarScalarFactor μ μ = 1 :=
by
by_cases hG : LocallyCompactSpace G; swap
· simp [haarScalarFactor, hG]
obtain ⟨⟨g, g_cont⟩, g_comp, g_nonneg, g_one⟩ : ∃ g : C(G, ℝ), HasCompactSupport g ∧ 0 ≤ g ∧ g 1 ≠ 0 :=
exists_continuous_nonneg_pos 1
have int_g_ne_zero : ∫ x, g x ∂μ ≠ 0 :=
ne_of_gt (g_cont.integral_pos_of_hasCompactSupport_nonneg_nonzero g_comp g_nonneg g_one)
apply NNReal.coe_injective
calc
haarScalarFactor μ μ = (∫ x, g x ∂μ) / ∫ x, g x ∂μ :=
haarScalarFactor_eq_integral_div _ _ g_cont g_comp int_g_ne_zero
_ = 1 := div_self int_g_ne_zero
