English
If μ is inner regular and locally compact, then comparison with any other invariant measure is controlled by haarScalarFactor.
Русский
Если μ внутренняя регулярность и локально компактна, сравнение с любой другой инвариантной мерой задаётся коэффициентом Haar.
LaTeX
$$$$ μ' s = haarScalarFactor μ' μ \\cdot μ s, \\; \\text{for measurable } s \\text{ with compact closure} $$$$
Lean4
/-- If an invariant measure is inner regular, then it gives less mass to sets with compact closure
than any other invariant measure, up to the scalar `haarScalarFactor μ' μ`.
Auxiliary lemma in the proof of the more general
`measure_isMulInvariant_eq_smul_of_isCompact_closure`, which gives equality for any
set with compact closure. -/
@[to_additive smul_measure_isAddInvariant_le_of_isCompact_closure /--
If an invariant measure is inner regular, then it gives less mass to sets with compact closure
than any other invariant measure, up to the scalar `addHaarScalarFactor μ' μ`.
Auxiliary lemma in the proof of the more general
`measure_isAddInvariant_eq_smul_of_isCompact_closure`, which gives equality for any
set with compact closure. -/
]
theorem smul_measure_isMulInvariant_le_of_isCompact_closure [LocallyCompactSpace G] (μ' μ : Measure G) [IsHaarMeasure μ]
[IsFiniteMeasureOnCompacts μ'] [IsMulLeftInvariant μ'] [InnerRegularCompactLTTop μ] {s : Set G}
(hs : MeasurableSet s) (h's : IsCompact (closure s)) : haarScalarFactor μ' μ • μ s ≤ μ' s :=
by
apply le_of_forall_lt (fun r hr ↦ ?_)
let ν := haarScalarFactor μ' μ • μ
have : ν s ≠ ∞ := ((measure_mono subset_closure).trans_lt h's.measure_lt_top).ne
obtain ⟨-, hf, ⟨f, f_cont, f_comp, rfl⟩, νf⟩ :
∃ K ⊆ s, (∃ f, Continuous f ∧ HasCompactSupport f ∧ K = f ⁻¹' { 1 }) ∧ r < ν K :=
innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_group ⟨hs, this⟩ r (by convert hr)
calc
r < ν (f ⁻¹' { 1 }) := νf
_ = μ' (f ⁻¹' { 1 }) := (measure_preimage_isMulLeftInvariant_eq_smul_of_hasCompactSupport _ _ f_cont f_comp).symm
_ ≤ μ' s := measure_mono hf
