# The second Borel-Cantelli lemma #

This file contains the second Borel-Cantelli lemma which states that, given a sequence of independent sets (sₙ) in a probability space, if ∑ n, μ sₙ = ∞, then the limsup of sₙ has measure 1. We employ a proof using Lévy's generalized Borel-Cantelli by choosing an appropriate filtration.

## Main result #

• ProbabilityTheory.measure_limsup_eq_one: the second Borel-Cantelli lemma.

Note: for the first Borel-Cantelli lemma, which holds in general measure spaces (not only in probability spaces), see MeasureTheory.measure_limsup_eq_zero.

theorem ProbabilityTheory.iIndepFun.indep_comap_natural_of_lt {Ω : Type u_1} {m0 : } {μ : } {ι : Type u_2} {β : Type u_3} [] [mβ : ] [] {f : ιΩβ} {i : ι} {j : ι} (hf : ∀ (i : ι), ) (hfi : ProbabilityTheory.iIndepFun (fun (x : ι) => ) f μ) (hij : i < j) :
theorem ProbabilityTheory.iIndepFun.condexp_natural_ae_eq_of_lt {Ω : Type u_1} {m0 : } {μ : } {ι : Type u_2} {β : Type u_3} [] [mβ : ] [] {f : ιΩβ} {i : ι} {j : ι} [] [] (hf : ∀ (i : ι), ) (hfi : ProbabilityTheory.iIndepFun (fun (x : ι) => ) f μ) (hij : i < j) :
MeasureTheory.condexp ( i) μ (f j) =ᵐ[μ] fun (x : Ω) => ∫ (x : Ω), f j xμ
theorem ProbabilityTheory.iIndepSet.condexp_indicator_filtrationOfSet_ae_eq {Ω : Type u_1} {m0 : } {μ : } {ι : Type u_2} [] {i : ι} {j : ι} {s : ιSet Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)) (hs : ) (hij : i < j) :
MeasureTheory.condexp ( i) μ ((s j).indicator fun (x : Ω) => 1) =ᵐ[μ] fun (x : Ω) => (μ (s j)).toReal
theorem ProbabilityTheory.measure_limsup_eq_one {Ω : Type u_1} {m0 : } {μ : } {s : Set Ω} (hsm : ∀ (n : ), MeasurableSet (s n)) (hs : ) (hs' : ∑' (n : ), μ (s n) = ) :
μ (Filter.limsup s Filter.atTop) = 1

The second Borel-Cantelli lemma: Given a sequence of independent sets (sₙ) such that ∑ n, μ sₙ = ∞, limsup sₙ has measure 1.