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 : 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 : ι) => mβ) f μ)
(hij : i < j)
:
ProbabilityTheory.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 Ω}
[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 : ι) => mβ) f μ)
(hij : i < j)
:
MeasureTheory.condexp (↑(MeasureTheory.Filtration.natural f hf) i) μ (f j) =ᶠ[MeasureTheory.Measure.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) μ
(Set.indicator (s j) fun (x : Ω) => 1) =ᶠ[MeasureTheory.Measure.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.