English
For two Haar measures μ and ν and μ' left-invariant, haarScalarFactor μ' ν equals haarScalarFactor μ' μ times haarScalarFactor μ ν.
Русский
Для двух мер Хаара μ и ν и левойInvariant μ', коэффициент haarScalarFactor μ' ν равен коэффициенту haarScalarFactor μ' μ, умноженному на haarScalarFactor μ ν.
LaTeX
$$$$\\mathrm{haarScalarFactor} (μ' , ν) = \\mathrm{haarScalarFactor} (μ', μ) \\cdot \\mathrm{haarScalarFactor} (μ , ν).$$$$
Lean4
@[to_additive addHaarScalarFactor_eq_integral_div]
theorem haarScalarFactor_eq_integral_div (μ' μ : Measure G) [IsHaarMeasure μ] [IsFiniteMeasureOnCompacts μ']
[IsMulLeftInvariant μ'] {f : G → ℝ} (hf : Continuous f) (h'f : HasCompactSupport f)
(int_nonzero : ∫ x, f x ∂μ ≠ 0) : haarScalarFactor μ' μ = (∫ x, f x ∂μ') / ∫ x, f x ∂μ :=
by
have := integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport μ' μ hf h'f
rw [integral_smul_nnreal_measure] at this
exact EuclideanDomain.eq_div_of_mul_eq_left int_nonzero this.symm
