LaTeX
$$$\\forall s\\,(MeasurableSet\\,s)\\; (μ\\,s < ∞)\\;\\forall ε>0:\\;\\exists F,U\\; (F\\subseteq s)\\land (s\\subseteq U)\\land IsClosed F\\land IsOpen U\\land μ\\,s \\le μ\\,F + ε \\land μ\\,U \\le μ\\,s + ε$$$
Lean4
/-- In a finite measure space, assume that any open set can be approximated from inside by closed
sets. Then the measure is weakly regular. -/
theorem weaklyRegular_of_finite [BorelSpace α] (μ : Measure α) [IsFiniteMeasure μ]
(H : InnerRegularWRT μ IsClosed IsOpen) : WeaklyRegular μ :=
by
have hfin : ∀ {s}, μ s ≠ ∞ := @(measure_ne_top μ)
suffices
∀ s, MeasurableSet s → ∀ ε, ε ≠ 0 → ∃ F, F ⊆ s ∧ ∃ U, U ⊇ s ∧ IsClosed F ∧ IsOpen U ∧ μ s ≤ μ F + ε ∧ μ U ≤ μ s + ε
by
refine
{ outerRegular := fun s hs r hr => ?_
innerRegular := H }
rcases exists_between hr with ⟨r', hsr', hr'r⟩
rcases this s hs _ (tsub_pos_iff_lt.2 hsr').ne' with ⟨-, -, U, hsU, -, hUo, -, H⟩
refine ⟨U, hsU, hUo, ?_⟩
rw [add_tsub_cancel_of_le hsr'.le] at H
exact H.trans_lt hr'r
apply MeasurableSet.induction_on_open
· intro U hU ε hε
rcases H.exists_subset_lt_add isClosed_empty hU hfin hε with ⟨F, hsF, hFc, hF⟩
exact
⟨F, hsF, U, Subset.rfl, hFc, hU, hF.le, le_self_add⟩
-- check for complements
· rintro s hs H ε hε
rcases H ε hε with ⟨F, hFs, U, hsU, hFc, hUo, hF, hU⟩
refine ⟨Uᶜ, compl_subset_compl.2 hsU, Fᶜ, compl_subset_compl.2 hFs, hUo.isClosed_compl, hFc.isOpen_compl, ?_⟩
simp only [measure_compl_le_add_iff, *, hUo.measurableSet, hFc.measurableSet, true_and]
-- check for disjoint unions
· intro s hsd hsm H ε ε0
have ε0' : ε / 2 ≠ 0 := (ENNReal.half_pos ε0).ne'
rcases ENNReal.exists_pos_sum_of_countable' ε0' ℕ with ⟨δ, δ0, hδε⟩
choose F hFs U hsU hFc hUo hF hU using fun n => H n (δ n) (δ0 n).ne'
have : Tendsto (fun t => (∑ k ∈ t, μ (s k)) + ε / 2) atTop (𝓝 <| μ (⋃ n, s n) + ε / 2) :=
by
rw [measure_iUnion hsd hsm]
exact Tendsto.add ENNReal.summable.hasSum tendsto_const_nhds
rcases (this.eventually <| lt_mem_nhds <| ENNReal.lt_add_right hfin ε0').exists with
⟨t, ht⟩
-- the approximating open set is constructed by taking for each `s n` an approximating open set
-- `U n` with measure at most `μ (s n) + δ n` for a summable `δ`, and taking the union of these.
refine
⟨⋃ k ∈ t, F k, iUnion_mono fun k => iUnion_subset fun _ => hFs _, ⋃ n, U n, iUnion_mono hsU,
isClosed_biUnion_finset fun k _ => hFc k, isOpen_iUnion hUo, ht.le.trans ?_, ?_⟩
·
calc
(∑ k ∈ t, μ (s k)) + ε / 2 ≤ ((∑ k ∈ t, μ (F k)) + ∑ k ∈ t, δ k) + ε / 2 :=
by
rw [← sum_add_distrib]
gcongr
apply hF
_ ≤ (∑ k ∈ t, μ (F k)) + ε / 2 + ε / 2 := by
gcongr
exact (ENNReal.sum_le_tsum _).trans hδε.le
_ = μ (⋃ k ∈ t, F k) + ε :=
by
rw [measure_biUnion_finset, add_assoc, ENNReal.add_halves]
exacts [fun k _ n _ hkn => (hsd hkn).mono (hFs k) (hFs n), fun k _ => (hFc k).measurableSet]
·
calc
μ (⋃ n, U n) ≤ ∑' n, μ (U n) := measure_iUnion_le _
_ ≤ ∑' n, (μ (s n) + δ n) := (ENNReal.tsum_le_tsum hU)
_ = μ (⋃ n, s n) + ∑' n, δ n := by rw [measure_iUnion hsd hsm, ENNReal.tsum_add]
_ ≤ μ (⋃ n, s n) + ε := add_le_add_left (hδε.le.trans ENNReal.half_le_self) _
