Sequences of sets with summable consecutive symmetric differences #
If consecutive sets of a sequence differ by sets of summable measure, the Borel--Cantelli lemma
shows that almost every point eventually stays inside the sets or eventually stays outside them.
Membership in the sets therefore converges almost everywhere to membership in their liminf.
This turns a sequence of approximate constructions whose corrections have summable mass into a
limiting set, as in the allocation of disjoint sets of prescribed mass in a laminar family.
Main statements #
theorem
TauCeti.MeasureTheory.ae_eventually_mem_iff_mem_liminf
{α : Type u_1}
{F : Type u_2}
[FunLike F (Set α) ENNReal]
[MeasureTheory.OuterMeasureClass F α]
{μ : F}
{s : ℕ → Set α}
(hs : ∑' (n : ℕ), μ (symmDiff (s (n + 1)) (s n)) ≠ ⊤)
:
∀ᵐ (x : α) ∂μ, ∀ᶠ (n : ℕ) in Filter.atTop, x ∈ s n ↔ x ∈ Filter.liminf s Filter.atTop
If consecutive sets of a sequence differ by sets of summable measure, then for almost every
point, membership in the sets is eventually the same as membership in their liminf.