English
For a measurable set s, μ'(f^{-1}{1}) equals haarScalarFactor μ' μ times μ(f^{-1}{1}) when f has compact support.
Русский
Для измеримого множества s верно: μ'(f^{-1}{1}) = haarScalarFactor μ' μ · μ(f^{-1}{1}) при наличии функций с компактной опорой.
LaTeX
$$$$μ' (f^{-1}({1})) = haarScalarFactor μ' μ \\cdot μ (f^{-1}({1})).$$$$
Lean4
@[to_additive mul_addHaarScalarFactor_smul]
theorem mul_haarScalarFactor_smul [LocallyCompactSpace G] (μ' μ : Measure G) [IsHaarMeasure μ]
[IsFiniteMeasureOnCompacts μ'] [IsMulLeftInvariant μ'] {c : ℝ≥0} (hc : c ≠ 0) :
haveI : IsHaarMeasure (c • μ) := IsHaarMeasure.nnreal_smul _ hc
c * haarScalarFactor μ' (c • μ) = haarScalarFactor μ' μ :=
by
have : IsHaarMeasure (c • μ) := IsHaarMeasure.nnreal_smul _ hc
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
c * haarScalarFactor μ' (c • μ) = c * ((∫ x, g x ∂μ') / ∫ x, g x ∂(c • μ)) := by
rw [haarScalarFactor_eq_integral_div _ _ g_cont g_comp (by simp [int_g_ne_zero, hc])]
_ = c * ((∫ x, g x ∂μ') / (c • ∫ x, g x ∂μ)) := by simp
_ = (∫ x, g x ∂μ') / (∫ x, g x ∂μ) :=
by
rw [NNReal.smul_def, smul_eq_mul, ← mul_div_assoc]
exact mul_div_mul_left (∫ (x : G), g x ∂μ') (∫ (x : G), g x ∂μ) (by simp [hc])
_ = μ'.haarScalarFactor μ := (haarScalarFactor_eq_integral_div _ _ g_cont g_comp int_g_ne_zero).symm
