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_atTop_eq_zero.

theorem ProbabilityTheory.iIndepFun.indep_comap_natural_of_lt {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {β : Type u_3} [LinearOrder ι] [mβ : MeasurableSpace β] [NormedAddCommGroup β] [BorelSpace β] {f : ι → Ω → β} {i j : ι} (hf : ∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)) (hfi : iIndepFun f μ) (hij : i < j) : Indep (MeasurableSpace.comap (f j) mβ) (↑(MeasureTheory.Filtration.natural f hf) i) μ

theorem ProbabilityTheory.iIndepFun.condExp_natural_ae_eq_of_lt {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {β : Type u_3} [LinearOrder ι] [mβ : MeasurableSpace β] [NormedAddCommGroup β] [BorelSpace β] {f : ι → Ω → β} {i j : ι} [SecondCountableTopology β] [CompleteSpace β] [NormedSpace ℝ β] (hf : ∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)) (hfi : iIndepFun f μ) (hij : i < j) : μ[f j | ↑(MeasureTheory.Filtration.natural f hf) i] =ᵐ[μ] fun (x : Ω) => ∫ (x : Ω), f j x ∂μ

theorem ProbabilityTheory.iIndepSet.condExp_indicator_filtrationOfSet_ae_eq {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} [LinearOrder ι] {i j : ι} {s : ι → Set Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)) (hs : iIndepSet s μ) (hij : i < j) : μ[(s j).indicator fun (x : Ω) => 1 | ↑(MeasureTheory.filtrationOfSet hsm) i] =ᵐ[μ] fun (x : Ω) => μ.real (s j)

theorem ProbabilityTheory.measure_limsup_eq_one {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ℕ → Set Ω} (hsm : ∀ (n : ℕ), MeasurableSet (s n)) (hs : iIndepSet s μ) (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.