# mathlib3documentation

probability.borel_cantelli

# The second Borel-Cantelli lemma #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• probability_theory.measure_limsup_eq_one: the second Borel-Cantelli lemma.
theorem probability_theory.Indep_fun.indep_comap_natural_of_lt {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ι : Type u_2} {β : Type u_3} [linear_order ι] [mβ : measurable_space β] [borel_space β] {f : ι Ω β} {i j : ι} (hf : (i : ι), ) (hfi : probability_theory.Indep_fun (λ (i : ι), mβ) f μ) (hij : i < j) :
i) μ
theorem probability_theory.Indep_fun.condexp_natural_ae_eq_of_lt {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ι : Type u_2} {β : Type u_3} [linear_order ι] [mβ : measurable_space β] [borel_space β] {f : ι Ω β} {i j : ι} [ β] (hf : (i : ι), ) (hfi : probability_theory.Indep_fun (λ (i : ι), mβ) f μ) (hij : i < j) :
(f j) =ᵐ[μ] λ (ω : Ω), (x : Ω), f j x μ
theorem probability_theory.Indep_set.condexp_indicator_filtration_of_set_ae_eq {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ι : Type u_2} [linear_order ι] {i j : ι} {s : ι set Ω} (hsm : (n : ι), measurable_set (s n)) (hs : μ) (hij : i < j) :
((s j).indicator (λ (ω : Ω), 1)) =ᵐ[μ] λ (ω : Ω), (μ (s j)).to_real
theorem probability_theory.measure_limsup_eq_one {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {s : set Ω} (hsm : (n : ), measurable_set (s n)) (hs : μ) (hs' : ∑' (n : ), μ (s n) = ) :
= 1

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