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 Ω}
[measure_theory.is_probability_measure μ]
{ι : Type u_2}
{β : Type u_3}
[linear_order ι]
[mβ : measurable_space β]
[normed_add_comm_group β]
[borel_space β]
{f : ι → Ω → β}
{i j : ι}
(hf : ∀ (i : ι), measure_theory.strongly_measurable (f i))
(hfi : probability_theory.Indep_fun (λ (i : ι), mβ) f μ)
(hij : i < j) :
probability_theory.indep (measurable_space.comap (f j) mβ) (⇑(measure_theory.filtration.natural f hf) i) μ
theorem
probability_theory.Indep_fun.condexp_natural_ae_eq_of_lt
{Ω : Type u_1}
{m0 : measurable_space Ω}
{μ : measure_theory.measure Ω}
[measure_theory.is_probability_measure μ]
{ι : Type u_2}
{β : Type u_3}
[linear_order ι]
[mβ : measurable_space β]
[normed_add_comm_group β]
[borel_space β]
{f : ι → Ω → β}
{i j : ι}
[topological_space.second_countable_topology β]
[complete_space β]
[normed_space ℝ β]
(hf : ∀ (i : ι), measure_theory.strongly_measurable (f i))
(hfi : probability_theory.Indep_fun (λ (i : ι), mβ) f μ)
(hij : i < j) :
measure_theory.condexp (⇑(measure_theory.filtration.natural f hf) i) μ (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 Ω}
[measure_theory.is_probability_measure μ]
{ι : Type u_2}
[linear_order ι]
{i j : ι}
{s : ι → set Ω}
(hsm : ∀ (n : ι), measurable_set (s n))
(hs : probability_theory.Indep_set s μ)
(hij : i < j) :
measure_theory.condexp (⇑(measure_theory.filtration_of_set hsm) i) μ ((s j).indicator (λ (ω : Ω), 1)) =ᵐ[μ] λ (ω : Ω), (⇑μ (s j)).to_real
theorem
probability_theory.measure_limsup_eq_one
{Ω : Type u_1}
{m0 : measurable_space Ω}
{μ : measure_theory.measure Ω}
[measure_theory.is_probability_measure μ]
{s : ℕ → set Ω}
(hsm : ∀ (n : ℕ), measurable_set (s n))
(hs : probability_theory.Indep_set s μ)
(hs' : ∑' (n : ℕ), ⇑μ (s n) = ⊤) :
⇑μ (filter.limsup s filter.at_top) = 1
The second Borel-Cantelli lemma: Given a sequence of independent sets (sₙ) such that
∑ n, μ sₙ = ∞, limsup sₙ has measure 1.