English
Let μ, μ′ be left-invariant measures which are finite on compacts; if μ and μ′ are regular, then μ′ = haarScalarFactor μ′ μ · μ.
Русский
Пусть μ и μ′ — лево-инвариантные меры, конечные на компактах; если обеregular, то μ′ = haarScalarFactor μ′ μ · μ.
LaTeX
$$$\\forall G \\; [LocallyCompactSpace G] \\; (μ' : \\mathrm{Measure}(G)) \\; (μ : \\mathrm{Measure}(G)) \\, [IsHaarMeasure μ] \\, [IsFiniteMeasureOnCompacts μ'] \\, [IsMulLeftInvariant μ'] \\, [Regular μ] \\, [Regular μ'] \\, μ' = haarScalarFactor μ' μ · μ$$
Lean4
theorem addHaarScalarFactor_domSMul (g : Gᵈᵐᵃ) : addHaarScalarFactor (g • μ) (g • ν) = addHaarScalarFactor μ ν :=
by
obtain ⟨⟨f, f_cont⟩, f_comp, f_nonneg, f_zero⟩ : ∃ f : C(A, ℝ), HasCompactSupport f ∧ 0 ≤ f ∧ f 0 ≠ 0 :=
exists_continuous_nonneg_pos 0
have int_f_ne_zero : ∫ x, f x ∂g • ν ≠ 0 :=
(f_cont.integral_pos_of_hasCompactSupport_nonneg_nonzero f_comp f_nonneg f_zero).ne'
apply NNReal.coe_injective
rw [addHaarScalarFactor_eq_integral_div (g • μ) (g • ν) f_cont f_comp int_f_ne_zero, integral_domSMul,
integral_domSMul]
refine (addHaarScalarFactor_eq_integral_div _ _ (by fun_prop) ?_ ?_).symm
· exact f_comp.comp_isClosedEmbedding (Homeomorph.smul _).isClosedEmbedding
· rw [← integral_domSMul]
exact (f_cont.integral_pos_of_hasCompactSupport_nonneg_nonzero f_comp f_nonneg f_zero).ne'
