Borel-Cantelli lemma, part 1

In this file we show one implication of the Borel-Cantelli lemma: if s i is a countable family of sets such that ∑' i, μ (s i) is finite, then a.e. all points belong to finitely many sets of the family.

We prove several versions of this lemma:

• MeasureTheory.ae_finite_setOf_mem: as stated above;
• MeasureTheory.measure_limsup_cofinite_eq_zero: in terms of Filter.limsup along Filter.cofinite;
• MeasureTheory.measure_limsup_atTop_eq_zero: in terms of Filter.limsup along (Filter.atTop : Filter ℕ).

For the second Borel-Cantelli lemma (applying to independent sets in a probability space), see ProbabilityTheory.measure_limsup_eq_one.

theorem MeasureTheory.measure_limsup_cofinite_eq_zero {α : Type u_1} {ι : Type u_2} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] [Countable ι] {μ : F} {s : ι → Set α} (hs : ∑' (i : ι), μ (s i) ≠ ⊤) : μ (Filter.limsup s Filter.cofinite) = 0

One direction of the Borel-Cantelli lemma (sometimes called the "first Borel-Cantelli lemma"): if (s i) is a countable family of sets such that ∑' i, μ (s i) is finite, then the limit superior of the s i along the cofinite filter is a null set.

Note: for the second Borel-Cantelli lemma (applying to independent sets in a probability space), see ProbabilityTheory.measure_limsup_eq_one.

theorem MeasureTheory.measure_limsup_atTop_eq_zero {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} {s : ℕ → Set α} (hs : ∑' (i : ℕ), μ (s i) ≠ ⊤) : μ (Filter.limsup s Filter.atTop) = 0

One direction of the Borel-Cantelli lemma (sometimes called the "first Borel-Cantelli lemma"): if (s i) is a sequence of sets such that ∑' i, μ (s i) is finite, then the limit superior of the s i along the atTop filter is a null set.

Note: for the second Borel-Cantelli lemma (applying to independent sets in a probability space), see ProbabilityTheory.measure_limsup_eq_one.

theorem MeasureTheory.ae_finite_setOf_mem {α : Type u_1} {ι : Type u_2} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] [Countable ι] {μ : F} {s : ι → Set α} (h : ∑' (i : ι), μ (s i) ≠ ⊤) : ∀ᵐ (x : α) ∂μ, {i : ι | x ∈ s i}.Finite

One direction of the Borel-Cantelli lemma (sometimes called the "first Borel-Cantelli lemma"): if (s i) is a countable family of sets such that ∑' i, μ (s i) is finite, then a.e. all points belong to finitely sets of the family.

theorem MeasureTheory.measure_setOf_frequently_eq_zero {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} {p : ℕ → α → Prop} (hp : ∑' (i : ℕ), μ {x : α | p i x} ≠ ⊤) : μ {x : α | ∃ᶠ (n : ℕ) in Filter.atTop, p n x} = 0

A version of the Borel-Cantelli lemma: if pᵢ is a sequence of predicates such that ∑' i, μ {x | pᵢ x} is finite, then the measure of x such that pᵢ x holds frequently as i → ∞ (or equivalently, pᵢ x holds for infinitely many i) is equal to zero.

theorem MeasureTheory.ae_eventually_notMem {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} {s : ℕ → Set α} (hs : ∑' (i : ℕ), μ (s i) ≠ ⊤) : ∀ᵐ (x : α) ∂μ, ∀ᶠ (n : ℕ) in Filter.atTop, x ∉ s n

A version of the Borel-Cantelli lemma: if sᵢ is a sequence of sets such that ∑' i, μ sᵢ is finite, then for almost all x, x does not belong to sᵢ for large i.

@[deprecated MeasureTheory.ae_eventually_notMem (since := "2025-05-23")]

theorem MeasureTheory.ae_eventually_not_mem {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} {s : ℕ → Set α} (hs : ∑' (i : ℕ), μ (s i) ≠ ⊤) : ∀ᵐ (x : α) ∂μ, ∀ᶠ (n : ℕ) in Filter.atTop, x ∉ s n

Alias of MeasureTheory.ae_eventually_notMem.

---

A version of the Borel-Cantelli lemma: if sᵢ is a sequence of sets such that ∑' i, μ sᵢ is finite, then for almost all x, x does not belong to sᵢ for large i.

theorem MeasureTheory.measure_liminf_cofinite_eq_zero {α : Type u_1} {ι : Type u_2} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] [Countable ι] {μ : F} [Infinite ι] {s : ι → Set α} (h : ∑' (i : ι), μ (s i) ≠ ⊤) : μ (Filter.liminf s Filter.cofinite) = 0

theorem MeasureTheory.measure_liminf_atTop_eq_zero {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} {s : ℕ → Set α} (h : ∑' (i : ℕ), μ (s i) ≠ ⊤) : μ (Filter.liminf s Filter.atTop) = 0

theorem MeasureTheory.limsup_ae_eq_of_forall_ae_eq {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} (s : ℕ → Set α) {t : Set α} (h : ∀ (n : ℕ), s n =ᶠ[ae μ] t) : Filter.limsup s Filter.atTop =ᶠ[ae μ] t

theorem MeasureTheory.liminf_ae_eq_of_forall_ae_eq {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} (s : ℕ → Set α) {t : Set α} (h : ∀ (n : ℕ), s n =ᶠ[ae μ] t) : Filter.liminf s Filter.atTop =ᶠ[ae μ] t