English
If μ' is scaled by a nonzero NRF c>0, then haarScalarFactor scales by c: haarScalarFactor(c•μ', μ) = c • haarScalarFactor(μ', μ).
Русский
Если меру μ' умножить на ненулевой NRF c>0, то скалярный фактор масштабает на c: haarScalarFactor(c•μ', μ) = c • haarScalarFactor(μ', μ).
LaTeX
$$$$\\mathrm{haarScalarFactor} (c \\cdot μ', μ) = c \\cdot \\mathrm{haarScalarFactor} (μ', μ).$$$$
Lean4
/-- Two left invariant measures integrate in the same way continuous compactly supported functions,
up to the scalar `haarScalarFactor μ' μ`. See also
`measure_isMulInvariant_eq_smul_of_isCompact_closure`, which gives the same result for compact
sets, and `measure_isHaarMeasure_eq_smul_of_isOpen` for open sets. -/
@[to_additive integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport /--
Two left invariant measures integrate in the same way continuous compactly supported functions,
up to the scalar `addHaarScalarFactor μ' μ`. See also
`measure_isAddInvariant_eq_smul_of_isCompact_closure`, which gives the same result for compact
sets, and `measure_isAddHaarMeasure_eq_smul_of_isOpen` for open sets. -/
]
theorem integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport (μ' μ : Measure G) [IsHaarMeasure μ]
[IsFiniteMeasureOnCompacts μ'] [IsMulLeftInvariant μ'] {f : G → ℝ} (hf : Continuous f) (h'f : HasCompactSupport f) :
∫ x, f x ∂μ' = ∫ x, f x ∂(haarScalarFactor μ' μ • μ) := by
classical
rcases h'f.eq_zero_or_locallyCompactSpace_of_group hf with Hf | Hf
· simp [Hf]
· simp only [haarScalarFactor, Hf, not_true_eq_false, ite_false]
exact (exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport μ' μ).choose_spec f hf h'f
