English
Let X be a measure space. If 𝒜 is a set algebra generating the measurable space, and there exists a monotone countable family of sets from 𝒜 with finite measure that spans X, then 𝒜 is measure-dense in X.
Русский
Пусть X — пространство меры, 𝒜 — множество алгебра множеств, порождающее σ-алгебу измеримости, и существует возрастающая по включению счетная последовательность множеств из 𝒜 с конечной мерой, чья объединяющая область покрывает X. Тогда 𝒜 плотна по мере μ на X.
LaTeX
$$$$ \text{IsSetAlgebra }\\mathcal{A} \\;\\to\\; μ.FiniteSpanningSetsIn 𝒜 \\;\\to\\; m = \\mathrm{MeasurableSpace.generateFrom } 𝒜 \\;\\to\\; μ.MeasureDense 𝒜. $$$$
Lean4
/-- If a measure space `X` is generated by an algebra of sets which contains a monotone countable
family of sets with finite measure spanning `X` (thus the measure is `σ`-finite), then this algebra
of sets is measure-dense. -/
theorem of_generateFrom_isSetAlgebra_sigmaFinite (h𝒜 : IsSetAlgebra 𝒜) (S : μ.FiniteSpanningSetsIn 𝒜)
(hgen : m = MeasurableSpace.generateFrom 𝒜) : μ.MeasureDense 𝒜
where
measurable s hs := hgen ▸ measurableSet_generateFrom hs
approx s ms hμs ε
ε_pos := by
-- We use partial unions of (Sₙ) to get a monotone family spanning `X`.
let T := Accumulate S.set
have T_mem (n) : T n ∈ 𝒜 := by simpa using h𝒜.biUnion_mem {k | k ≤ n}.toFinset (fun k _ ↦ S.set_mem k)
have T_finite (n) : μ (T n) < ∞ := by
simpa using measure_biUnion_lt_top {k | k ≤ n}.toFinset.finite_toSet (fun k _ ↦ S.finite k)
have T_spanning : ⋃ n, T n = univ := S.spanning ▸ iUnion_accumulate
have mono : Monotone (fun n ↦ (T n) ∩ s) := fun m n hmn ↦
inter_subset_inter_left s (biUnion_subset_biUnion_left fun k hkm ↦ Nat.le_trans hkm hmn)
have := tendsto_measure_iUnion_atTop (μ := μ) mono
rw [← tendsto_toReal_iff] at this
· -- We can therefore choose `N` such that `μ s - μ ((S N) ∩ s) < ε/2`.
rcases Metric.tendsto_atTop.1 this (ε / 2) (by linarith [ε_pos]) with ⟨N, hN⟩
have : Fact (μ (T N) < ∞) := Fact.mk <| T_finite N
rcases
(Measure.MeasureDense.of_generateFrom_isSetAlgebra_finite (μ.restrict (T N)) h𝒜 hgen).approx s ms
(ne_of_lt (lt_of_le_of_lt (μ.restrict_apply_le _ s) hμs.lt_top)) (ε / 2) (by linarith [ε_pos]) with
⟨t, t_mem, ht⟩
-- We can then use `t ∩ (S N)`, because `S N ∈ 𝒜` by hypothesis.
-- `μ (s ∆ (t ∩ S N))`
-- `≤ μ (s ∆ (s ∩ S N)) + μ ((s ∩ S N) ∆ (t ∩ S N))`
-- `= μ s - μ (s ∩ S N) + μ (s ∆ t) ∩ S N) < ε`.
refine ⟨t ∩ T N, h𝒜.inter_mem t_mem (T_mem N), ?_⟩
calc
μ (s ∆ (t ∩ T N)) ≤ μ (s \ (s ∩ T N)) + μ ((s ∆ t) ∩ T N) :=
by
rw [← symmDiff_of_le (inter_subset_left ..), symmDiff_comm _ s, inter_symmDiff_distrib_right]
exact measure_symmDiff_le _ _ _
_ < ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2) :=
by
apply ENNReal.add_lt_add
· rw [measure_diff (inter_subset_left ..)
(ms.inter (hgen ▸ measurableSet_generateFrom (T_mem N))).nullMeasurableSet
(ne_top_of_le_ne_top hμs (measure_mono (inter_subset_left ..))),
lt_ofReal_iff_toReal_lt (sub_ne_top hμs), toReal_sub_of_le (measure_mono (inter_subset_left ..)) hμs]
apply lt_of_le_of_lt (sub_le_dist ..)
nth_rw 1 [← univ_inter s]
rw [inter_comm s, dist_comm, ← T_spanning, iUnion_inter _ T]
apply hN N (le_refl _)
· rwa [← μ.restrict_apply' (hgen ▸ measurableSet_generateFrom (T_mem N))]
_ = ENNReal.ofReal ε := by rw [← ofReal_add (by linarith [ε_pos]) (by linarith [ε_pos]), add_halves]
· exact fun n ↦ ne_top_of_le_ne_top hμs (measure_mono (inter_subset_right ..))
· exact ne_top_of_le_ne_top hμs (measure_mono (iUnion_subset (fun i ↦ inter_subset_right ..)))
