English
There exists a scalar c≥0 such that for every continuous compactly supported f, ∫ f dμ' = c ∫ f dμ.
Русский
Существует константа c≥0 такая, что для каждой непрерывной функции с компактной опорой выполняется ∫ f dμ' = c ∫ f dμ.
LaTeX
$$$$\\exists c \\ge 0, \\; ∀ f: G \\to \\mathbb{R}, \\; \\text{Continuous}(f) \\land \\text{HasCompactSupport}(f) \\Rightarrow \\int_G f \\, dμ' = c \\cdot \\int_G f \\, dμ.$$$$
Lean4
/-- Given two left-invariant measures which are finite on
compacts, they coincide in the following sense: they give the same value to the integral of
continuous compactly supported functions, up to a multiplicative constant. -/
@[to_additive exists_integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport]
theorem exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport (μ' μ : Measure G) [IsHaarMeasure μ]
[IsFiniteMeasureOnCompacts μ'] [IsMulLeftInvariant μ'] :
∃ (c : ℝ≥0), ∀ (f : G → ℝ), Continuous f → HasCompactSupport f → ∫ x, f x ∂μ' = ∫ x, f x ∂(c • μ) := by
-- The group has to be locally compact, otherwise all integrals vanish and the result is trivial.
by_cases H : LocallyCompactSpace G; swap
· refine ⟨0, fun f f_cont f_comp ↦ ?_⟩
rcases f_comp.eq_zero_or_locallyCompactSpace_of_group f_cont with hf | hf
· simp [hf]
· exact (H hf).elim
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_pos : 0 < ∫ x, g x ∂μ := g_cont.integral_pos_of_hasCompactSupport_nonneg_nonzero g_comp g_nonneg g_one
let c : ℝ := (∫ x, g x ∂μ)⁻¹ * (∫ x, g x ∂μ')
have c_nonneg : 0 ≤ c := mul_nonneg (inv_nonneg.2 (integral_nonneg g_nonneg)) (integral_nonneg g_nonneg)
refine
⟨⟨c, c_nonneg⟩, fun f f_cont f_comp ↦ ?_⟩
/- use the lemma `integral_mulLeftInvariant_mulRightInvariant_combo` for `μ` and then `μ'`
to reexpress the integral of `f` as the integral of `g` times a factor which only depends
on a right-invariant measure `ν`. We use `ν = μ.inv` for convenience. -/
let ν := μ.inv
have A : ∫ x, f x ∂μ = (∫ y, f y * (∫ z, g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) * ∫ x, g x ∂μ :=
integral_isMulLeftInvariant_isMulRightInvariant_combo f_cont f_comp g_cont g_comp g_nonneg g_one
rw [← mul_inv_eq_iff_eq_mul₀ int_g_pos.ne'] at A
have B : ∫ x, f x ∂μ' = (∫ y, f y * (∫ z, g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) * ∫ x, g x ∂μ' :=
integral_isMulLeftInvariant_isMulRightInvariant_combo f_cont f_comp g_cont g_comp g_nonneg g_one
rw [← A, mul_assoc, mul_comm] at B
simp [B, integral_smul_nnreal_measure, c, NNReal.smul_def]
