Lean4
/-- If a measurable space equipped with a finite measure is generated by an algebra of sets, then
this algebra of sets is measure-dense. -/
theorem of_generateFrom_isSetAlgebra_finite [IsFiniteMeasure μ] (h𝒜 : IsSetAlgebra 𝒜)
(hgen : m = MeasurableSpace.generateFrom 𝒜) : μ.MeasureDense 𝒜
where
measurable s hs := hgen ▸ measurableSet_generateFrom hs
approx s
ms := by
-- We want to show that any measurable set can be approximated by sets in `𝒜`. To do so, it is
-- enough to show that such sets constitute a `σ`-algebra containing `𝒜`. This is contained in
-- the theorem `generateFrom_induction`.
have : MeasurableSet s ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (s ∆ t) < ε :=
by
rw [hgen] at ms
induction s, ms using generateFrom_induction with
-- If `t ∈ 𝒜`, then `μ (t ∆ t) = 0` which is less than any `ε > 0`.
| hC t t_mem _ =>
exact
⟨hgen ▸ measurableSet_generateFrom t_mem, fun ε ε_pos ↦ ⟨t, t_mem, by simpa⟩⟩
-- `∅ ∈ 𝒜` and `μ (∅ ∆ ∅) = 0` which is less than any `ε > 0`.
| empty =>
exact
⟨MeasurableSet.empty, fun ε ε_pos ↦ ⟨∅, h𝒜.empty_mem, by simpa⟩⟩
-- If `s` is measurable and `t ∈ 𝒜` such that `μ (s ∆ t) < ε`, then `tᶜ ∈ 𝒜` and
-- `μ (sᶜ ∆ tᶜ) = μ (s ∆ t) < ε` so `sᶜ` can be approximated.
| compl t _ ht =>
refine ⟨ht.1.compl, fun ε ε_pos ↦ ?_⟩
obtain ⟨u, u_mem, hμtcu⟩ := ht.2 ε ε_pos
exact
⟨uᶜ, h𝒜.compl_mem u_mem, by rwa [compl_symmDiff_compl]⟩
-- Let `(fₙ)` be a sequence of measurable sets and `ε > 0`.
| iUnion f _
hf =>
refine
⟨MeasurableSet.iUnion (fun n ↦ (hf n).1), fun ε ε_pos ↦ ?_⟩
-- We have `μ (⋃ n ≤ N, fₙ) ⟶ μ (⋃ n, fₙ)`.
have := tendsto_measure_iUnion_accumulate (μ := μ) (f := f)
rw [← tendsto_toReal_iff (fun _ ↦ measure_ne_top _ _) (measure_ne_top _ _)] at this
rcases Metric.tendsto_atTop.1 this (ε / 2) (by linarith [ε_pos]) with
⟨N, hN⟩
-- For any `n ≤ N` there exists `gₙ ∈ 𝒜` such that `μ (fₙ ∆ gₙ) < ε/(2*(N+1))`.
choose g g_mem hg using fun n ↦
(hf n).2 (ε / (2 * (N + 1)))
(div_pos ε_pos (by linarith))
-- Therefore we have
-- `μ ((⋃ n, fₙ) ∆ (⋃ n ≤ N, gₙ))`
-- `≤ μ ((⋃ n, fₙ) ∆ (⋃ n ≤ N, fₙ)) + μ ((⋃ n ≤ N, fₙ) ∆ (⋃ n ≤ N, gₙ))`
-- `< ε/2 + ∑ n ≤ N, μ (fₙ ∆ gₙ)` (see `biSup_symmDiff_biSup_le`)
-- `< ε/2 + (N+1)*ε/(2*(N+1)) = ε/2`.
refine ⟨⋃ n ∈ Finset.range (N + 1), g n, h𝒜.biUnion_mem _ (fun i _ ↦ g_mem i), ?_⟩
calc
μ.real ((⋃ n, f n) ∆ (⋃ n ∈ (Finset.range (N + 1)), g n)) ≤
(μ
((⋃ n, f n) \ ((⋃ n ∈ (Finset.range (N + 1)), f n)) ∪
((⋃ n ∈ (Finset.range (N + 1)), f n) ∆ (⋃ n ∈ (Finset.range (N + 1)), g ↑n)))).toReal :=
toReal_mono (measure_ne_top _ _)
(measure_mono <|
symmDiff_of_ge (iUnion_subset <| fun i ↦ iUnion_subset (fun _ ↦ subset_iUnion f i)) ▸
symmDiff_triangle ..)
_ ≤
(μ ((⋃ n, f n) \ ((⋃ n ∈ (Finset.range (N + 1)), f n)))).toReal +
(μ ((⋃ n ∈ (Finset.range (N + 1)), f n) ∆ (⋃ n ∈ (Finset.range (N + 1)), g ↑n))).toReal :=
by
rw [← toReal_add (measure_ne_top _ _) (measure_ne_top _ _)]
exact toReal_mono (add_ne_top.2 ⟨measure_ne_top _ _, measure_ne_top _ _⟩) <| measure_union_le _ _
_ < ε := by
rw [← add_halves ε]
apply _root_.add_lt_add
· rw [measure_diff (h_fin := measure_ne_top _ _), toReal_sub_of_le (ha := measure_ne_top _ _)]
· apply lt_of_le_of_lt (sub_le_dist ..)
simp only [Finset.mem_range, Nat.lt_add_one_iff]
exact (dist_comm (α := ℝ) .. ▸ hN N (le_refl N))
· exact measure_mono <| iUnion_subset <| fun i ↦ iUnion_subset fun _ ↦ subset_iUnion f i
· exact iUnion_subset <| fun i ↦ iUnion_subset (fun _ ↦ subset_iUnion f i)
· exact MeasurableSet.biUnion (countable_coe_iff.1 inferInstance) (fun n _ ↦ (hf n).1.nullMeasurableSet)
·
calc
(μ ((⋃ n ∈ (Finset.range (N + 1)), f n) ∆ (⋃ n ∈ (Finset.range (N + 1)), g ↑n))).toReal ≤
μ.real (⋃ n ∈ (Finset.range (N + 1)), f n ∆ g n) :=
toReal_mono (measure_ne_top _ _) (measure_mono biSup_symmDiff_biSup_le)
_ ≤ ∑ n ∈ Finset.range (N + 1), μ.real (f n ∆ g n) :=
by
simp_rw [measureReal_def, ← toReal_sum (fun _ _ ↦ measure_ne_top _ _)]
exact
toReal_mono (ne_of_lt <| sum_lt_top.2 fun _ _ ↦ measure_lt_top μ _) (measure_biUnion_finset_le _ _)
_ < ∑ n ∈ Finset.range (N + 1), (ε / (2 * (N + 1))) :=
(Finset.sum_lt_sum (fun i _ ↦ le_of_lt (hg i)) ⟨0, by simp, hg 0⟩)
_ ≤ ε / 2 :=
by
simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul, Nat.cast_add, Nat.cast_one]
rw [div_mul_eq_div_mul_one_div, ← mul_assoc, mul_comm ((N : ℝ) + 1), mul_assoc]
exact
mul_le_of_le_one_right (by linarith [ε_pos]) <|
le_of_eq <| mul_one_div_cancel <| Nat.cast_add_one_ne_zero _
rintro - ε ε_pos
rcases this.2 ε ε_pos with ⟨t, t_mem, hμst⟩
exact ⟨t, t_mem, (lt_ofReal_iff_toReal_lt (measure_ne_top _ _)).2 hμst⟩
