English
The Haar scalar factor is multiplicative along a chain of Haar measures: Haar μ' ν = Haar μ' μ × Haar μ ν.
Русский
Коэффициент Хаара мультипликативен вдоль цепочки мер: Haar μ' ν = Haar μ' μ × Haar μ ν.
LaTeX
$$$$ \\mathrm{haarScalarFactor}(μ', ν) = \\mathrm{haarScalarFactor}(μ', μ) \\cdot \\mathrm{haarScalarFactor}(μ, ν). $$$$
Lean4
@[to_additive addHaarScalarFactor_eq_mul]
theorem haarScalarFactor_eq_mul (μ' μ ν : Measure G) [IsHaarMeasure μ] [IsHaarMeasure ν] [IsFiniteMeasureOnCompacts μ']
[IsMulLeftInvariant μ'] : haarScalarFactor μ' ν = haarScalarFactor μ' μ * haarScalarFactor μ ν := by
-- The group has to be locally compact, otherwise the scalar factor is 1 by definition.
by_cases hG : LocallyCompactSpace G; swap
·
simp [haarScalarFactor, hG]
-- Fix some nonzero continuous function with compact support `g`.
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 Z := integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport μ' μ g_cont g_comp
simp only [integral_smul_nnreal_measure, smul_smul,
integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport μ' ν g_cont g_comp,
integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport μ ν g_cont g_comp] at Z
have int_g_pos : 0 < ∫ x, g x ∂ν :=
by
apply (integral_pos_iff_support_of_nonneg g_nonneg _).2
· exact IsOpen.measure_pos ν g_cont.isOpen_support ⟨1, g_one⟩
· exact g_cont.integrable_of_hasCompactSupport g_comp
change
(haarScalarFactor μ' ν : ℝ) * ∫ (x : G), g x ∂ν =
(haarScalarFactor μ' μ * haarScalarFactor μ ν : ℝ≥0) * ∫ (x : G), g x ∂ν at Z
simpa only [mul_eq_mul_right_iff (M₀ := ℝ), int_g_pos.ne', or_false, ← NNReal.eq_iff] using Z
