English
The definition haarScalarFactor(μ', μ) is the factor that links the integrals of compactly supported functions under μ' and μ when both are left-invariant; LocallyCompact or not, it defaults to 1 if not locally compact.
Русский
Определение haarScalarFactor(μ', μ) — это коэффициент, связывающий интегралы по μ' и μ для компактноопорных функций; если группа локально компактна — соответствующий коэффициент существует; в противном случае берётся 1.
LaTeX
$$$$\\text{haarScalarFactor} (μ', μ) :\\mathbb{R}_{\\ge 0} $$, with the property that for all continuous compactly supported f, ∫ f dμ' = haarScalarFactor(μ', μ) · ∫ f dμ.$$
Lean4
/-- Given two left-invariant measures which are finite on compacts, `haarScalarFactor μ' μ` is a
scalar such that `∫ f dμ' = (haarScalarFactor μ' μ) ∫ f dμ` for any compactly supported continuous
function `f`.
Note that there is a dissymmetry in the assumptions between `μ'` and `μ`: the measure `μ'` needs
only be finite on compact sets, while `μ` has to be finite on compact sets and positive on open
sets, i.e., a Haar measure, to exclude for instance the case where `μ = 0`, where the definition
doesn't make sense. -/
@[to_additive /-- Given two left-invariant measures which are finite on compacts,
`addHaarScalarFactor μ' μ` is a scalar such that `∫ f dμ' = (addHaarScalarFactor μ' μ) ∫ f dμ` for
any compactly supported continuous function `f`.
Note that there is a dissymmetry in the assumptions between `μ'` and `μ`: the measure `μ'` needs
only be finite on compact sets, while `μ` has to be finite on compact sets and positive on open
sets, i.e., an additive Haar measure, to exclude for instance the case where `μ = 0`, where the
definition doesn't make sense. -/
]
noncomputable def haarScalarFactor (μ' μ : Measure G) [IsHaarMeasure μ] [IsFiniteMeasureOnCompacts μ']
[IsMulLeftInvariant μ'] : ℝ≥0 :=
if ¬LocallyCompactSpace G then 1 else (exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport μ' μ).choose
