English
If μ and μ' are invariant and μ is inner regular, then for any set s with compact closure, μ'(s) = haarScalarFactor μ' μ · μ(s).
Русский
Если μ и μ' инвариантны, а μ внутренняя регулярность, то для любого множества s с компактным замыканием выполняется μ'(s) = haarScalarFactor μ' μ · μ(s).
LaTeX
$$$$ μ'(s) = haarScalarFactor μ' μ \\cdot μ(s) $$, для с f closure(s) компактно.$$
Lean4
/-- If an invariant measure is inner regular, then it gives the same mass to measurable sets with
compact closure as 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 works for any set with
compact closure, and removes the inner regularity assumption. -/
@[to_additive measure_isAddInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop /--
If an invariant measure is inner regular, then it gives the same mass to measurable sets with
compact closure as 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 works for any set with
compact closure, and removes the inner regularity assumption. -/
]
theorem measure_isMulInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop [LocallyCompactSpace G]
(μ' μ : Measure G) [IsHaarMeasure μ] [IsFiniteMeasureOnCompacts μ'] [IsMulLeftInvariant μ']
[InnerRegularCompactLTTop μ] {s : Set G} (hs : MeasurableSet s) (h's : IsCompact (closure s)) :
μ' s = haarScalarFactor μ' μ • μ s :=
by
apply le_antisymm ?_ (smul_measure_isMulInvariant_le_of_isCompact_closure μ' μ hs h's)
let ν := haarScalarFactor μ' μ • μ
change μ' s ≤ ν s
obtain ⟨⟨f, f_cont⟩, hf, -, f_comp, -⟩ :
∃ f : C(G, ℝ), EqOn f 1 (closure s) ∧ EqOn f 0 ∅ ∧ HasCompactSupport f ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 :=
exists_continuous_one_zero_of_isCompact h's isClosed_empty (disjoint_empty _)
let t := f ⁻¹' { 1 }
have t_closed : IsClosed t := isClosed_singleton.preimage f_cont
have t_comp : IsCompact t := f_comp.isCompact_preimage f_cont isClosed_singleton (by simp)
have st : s ⊆ t := (IsClosed.closure_subset_iff t_closed).mp hf
have A : ν (t \ s) ≤ μ' (t \ s) :=
by
apply smul_measure_isMulInvariant_le_of_isCompact_closure _ _ (t_closed.measurableSet.diff hs)
exact t_comp.closure_of_subset diff_subset
have B : μ' t = ν t := measure_preimage_isMulLeftInvariant_eq_smul_of_hasCompactSupport _ _ f_cont f_comp
rwa [measure_diff st hs.nullMeasurableSet, measure_diff st hs.nullMeasurableSet, ← B,
ENNReal.sub_le_sub_iff_left] at A
· exact measure_mono st
· exact t_comp.measure_lt_top.ne
· exact ((measure_mono st).trans_lt t_comp.measure_lt_top).ne
· exact ((measure_mono st).trans_lt t_comp.measure_lt_top).ne
