English
If a measure, restricted to each of countably many open sets that cover the space, is outer regular, then the original measure is outer regular.
Русский
Если мера, ограниченная до каждой из счетной совокупности открытых покрытий, внешне регулярна, то и исходная мера внешне регулярна.
LaTeX
$$$OuterRegular(μ) \text{ on the space if } (μ|s_n)\text{ OuterRegular for all }n, \text{ and } ⋃ s_n = U$.$$
Lean4
/-- If the restrictions of a measure to countably many open sets covering the space are
outer regular, then the measure itself is outer regular. -/
theorem of_restrict [OpensMeasurableSpace α] {μ : Measure α} {s : ℕ → Set α} (h : ∀ n, OuterRegular (μ.restrict (s n)))
(h' : ∀ n, IsOpen (s n)) (h'' : univ ⊆ ⋃ n, s n) : OuterRegular μ :=
by
refine ⟨fun A hA r hr => ?_⟩
have HA : μ A < ∞ := lt_of_lt_of_le hr le_top
have hm : ∀ n, MeasurableSet (s n) := fun n => (h' n).measurableSet
obtain ⟨A, hAm, hAs, hAd, rfl⟩ :
∃ A' : ℕ → Set α, (∀ n, MeasurableSet (A' n)) ∧ (∀ n, A' n ⊆ s n) ∧ Pairwise (Disjoint on A') ∧ A = ⋃ n, A' n :=
by
refine
⟨fun n => A ∩ disjointed s n, fun n => hA.inter (MeasurableSet.disjointed hm _), fun n =>
inter_subset_right.trans (disjointed_subset _ _),
(disjoint_disjointed s).mono fun k l hkl => hkl.mono inf_le_right inf_le_right, ?_⟩
rw [← inter_iUnion, iUnion_disjointed, univ_subset_iff.mp h'', inter_univ]
rcases ENNReal.exists_pos_sum_of_countable' (tsub_pos_iff_lt.2 hr).ne' ℕ with ⟨δ, δ0, hδε⟩
rw [lt_tsub_iff_right, add_comm] at hδε
have : ∀ n, ∃ U ⊇ A n, IsOpen U ∧ μ U < μ (A n) + δ n :=
by
intro n
have H₁ : ∀ t, μ.restrict (s n) t = μ (t ∩ s n) := fun t => restrict_apply' (hm n)
have Ht : μ.restrict (s n) (A n) ≠ ∞ := by
rw [H₁]
exact ((measure_mono (inter_subset_left.trans (subset_iUnion A n))).trans_lt HA).ne
rcases (A n).exists_isOpen_lt_add Ht (δ0 n).ne' with ⟨U, hAU, hUo, hU⟩
rw [H₁, H₁, inter_eq_self_of_subset_left (hAs _)] at hU
exact ⟨U ∩ s n, subset_inter hAU (hAs _), hUo.inter (h' n), hU⟩
choose U hAU hUo hU using this
refine ⟨⋃ n, U n, iUnion_mono hAU, isOpen_iUnion hUo, ?_⟩
calc
μ (⋃ n, U n) ≤ ∑' n, μ (U n) := measure_iUnion_le _
_ ≤ ∑' n, (μ (A n) + δ n) := (ENNReal.tsum_le_tsum fun n => (hU n).le)
_ = ∑' n, μ (A n) + ∑' n, δ n := ENNReal.tsum_add
_ = μ (⋃ n, A n) + ∑' n, δ n := (congr_arg₂ (· + ·) (measure_iUnion hAd hAm).symm rfl)
_ < r := hδε
