Documentation

Mathlib.Probability.BorelCantelli

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 #

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 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ι : Type u_2} {β : Type u_3} [LinearOrder ι] [mβ : MeasurableSpace β] [NormedAddCommGroup β] [BorelSpace β] {f : ιΩβ} {i : ι} {j : ι} (hf : ∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)) (hfi : ProbabilityTheory.iIndepFun (fun (x : ι) => ) f μ) (hij : i < j) :
theorem ProbabilityTheory.iIndepFun.condexp_natural_ae_eq_of_lt {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ι : Type u_2} {β : Type u_3} [LinearOrder ι] [mβ : MeasurableSpace β] [NormedAddCommGroup β] [BorelSpace β] {f : ιΩβ} {i : ι} {j : ι} [SecondCountableTopology β] [CompleteSpace β] [NormedSpace β] (hf : ∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)) (hfi : ProbabilityTheory.iIndepFun (fun (x : ι) => ) f μ) (hij : i < j) :
MeasureTheory.condexp ((MeasureTheory.Filtration.natural f hf) i) μ (f j) =ᶠ[μ.ae] fun (x : Ω) => ∫ (x : Ω), f j xμ
theorem ProbabilityTheory.iIndepSet.condexp_indicator_filtrationOfSet_ae_eq {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ι : Type u_2} [LinearOrder ι] {i : ι} {j : ι} {s : ιSet Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)) (hs : ProbabilityTheory.iIndepSet s μ) (hij : i < j) :
MeasureTheory.condexp ((MeasureTheory.filtrationOfSet hsm) i) μ ((s j).indicator fun (x : Ω) => 1) =ᶠ[μ.ae] fun (x : Ω) => (μ (s j)).toReal
theorem ProbabilityTheory.measure_limsup_eq_one {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {s : Set Ω} (hsm : ∀ (n : ), MeasurableSet (s n)) (hs : ProbabilityTheory.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.