English
Under suitable hypotheses on G and μ, Haar measure is inner regular with respect to preimages of 1 under continuous functions with compact support; this yields a representation of finite-measure sets by such level sets with the same measure.
Русский
При разумных гипотезах относительно группы G и мере μ, мера Хаара обладает внутренней регулярностью через предобраз единицы непрерывных функций с компактной опорой; это дает представление множеств конечной меры через такие уровни, сохраняя меру.
LaTeX
$$InnerRegularWRT μ (λ s ↦ ∃ f : G → ℝ, Continuous f ∧ HasCompactSupport f ∧ s = f ⁻¹' { 1 }) (fun s ↦ MeasurableSet s ∧ μ s ≠ ∞)$$
Lean4
/-- **Halmos' theorem: Haar measure is completion regular.** More precisely, any finite measure
set can be approximated from inside by a level set of a continuous function with compact support. -/
@[to_additive innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_addGroup]
theorem innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_group :
InnerRegularWRT μ (fun s ↦ ∃ (f : G → ℝ), Continuous f ∧ HasCompactSupport f ∧ s = f ⁻¹' { 1 })
(fun s ↦ MeasurableSet s ∧ μ s ≠ ∞) :=
by
/- First, approximate a measurable set from inside by a compact closed set `K`. Then notice that
the everywhere positive subset of `K` is a Gδ,
by Lemma `IsEverywherePos.IsGdelta_of_isMulLeftInvariant`, and therefore the level set of a
continuous compactly supported function. Moreover, it has the same measure as `K`. -/
apply InnerRegularWRT.trans _ innerRegularWRT_isCompact_isClosed_measure_ne_top_of_group
intro K ⟨K_comp, K_closed⟩ r hr
let L := μ.everywherePosSubset K
have L_comp : IsCompact L := K_comp.everywherePosSubset
have L_closed : IsClosed L := K_closed.everywherePosSubset
refine ⟨L, everywherePosSubset_subset μ K, ?_, ?_⟩
· have : μ.IsEverywherePos L :=
isEverywherePos_everywherePosSubset_of_measure_ne_top K_closed.measurableSet K_comp.measure_lt_top.ne
have L_Gδ : IsGδ L := this.IsGdelta_of_isMulLeftInvariant L_comp L_closed
obtain ⟨⟨f, f_cont⟩, Lf, -, f_comp, -⟩ :
∃ f : C(G, ℝ), L = f ⁻¹' { 1 } ∧ EqOn f 0 ∅ ∧ HasCompactSupport f ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 :=
exists_continuous_one_zero_of_isCompact_of_isGδ L_comp L_Gδ isClosed_empty (disjoint_empty L)
exact ⟨f, f_cont, f_comp, Lf⟩
· convert hr using 1
apply measure_congr
exact everywherePosSubset_ae_eq_of_measure_ne_top K_closed.measurableSet K_comp.measure_lt_top.ne
