English
In the non-additive/ add-add dual version, the unfolding trick and scalar factors have additive analogues for additive groups.
Русский
В аддитивном аналоге аналогичные развёртывания и коэффициенты существуют для аддитивных групп.
LaTeX
$$$$\\text{(additive analogues of unfolding and Haar scalar factors)}$$$$
Lean4
@[to_additive (attr := simp) addHaarScalarFactor_smul]
theorem haarScalarFactor_smul [LocallyCompactSpace G] (μ' μ : Measure G) [IsHaarMeasure μ]
[IsFiniteMeasureOnCompacts μ'] [IsMulLeftInvariant μ'] {c : ℝ≥0} :
haarScalarFactor (c • μ') μ = c • haarScalarFactor μ' μ :=
by
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 (c • μ') μ = (∫ x, g x ∂(c • μ')) / ∫ x, g x ∂μ :=
haarScalarFactor_eq_integral_div _ _ g_cont g_comp int_g_ne_zero
_ = (c • (∫ x, g x ∂μ')) / ∫ x, g x ∂μ := by simp
_ = c • ((∫ x, g x ∂μ') / ∫ x, g x ∂μ) := (smul_div_assoc c _ _)
_ = c • haarScalarFactor μ' μ := by rw [← haarScalarFactor_eq_integral_div _ _ g_cont g_comp int_g_ne_zero]
