Kolmogorov's 0-1 law #
Let s : ι → MeasurableSpace Ω be an independent sequence of sub-σ-algebras. Then any set which
is measurable with respect to the tail σ-algebra limsup s atTop has probability 0 or 1.
Main statements #
measure_zero_or_one_of_measurableSet_limsup_atTop: Kolmogorov's 0-1 law. Any set which is measurable with respect to the tail σ-algebralimsup s atTopof an independent sequence of σ-algebrasshas probability 0 or 1.
theorem
ProbabilityTheory.measure_eq_zero_or_one_or_top_of_indepSet_self
{Ω : Type u_1}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{t : Set Ω}
(h_indep : ProbabilityTheory.IndepSet t t)
:
theorem
ProbabilityTheory.measure_eq_zero_or_one_of_indepSetCat_self
{Ω : Type u_1}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{t : Set Ω}
(h_indep : ProbabilityTheory.IndepSet t t)
:
theorem
ProbabilityTheory.indep_biSup_compl
{Ω : Type u_1}
{ι : Type u_2}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{s : ι → MeasurableSpace Ω}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.iIndep s)
(t : Set ι)
:
ProbabilityTheory.Indep (⨆ (n : ι) (_ : n ∈ t), s n) (⨆ (n : ι) (_ : n ∈ tᶜ), s n)
We prove a version of Kolmogorov's 0-1 law for the σ-algebra limsup s f where f is a filter
for which we can define the following two functions:
p : Set ι → Propsuch that for a sett,p t → tᶜ ∈ f,ns : α → Set ιa directed sequence of sets which all verifypand such that⋃ a, ns a = Set.univ.
For the example of f = atTop, we can take
p = bddAbove and ns : ι → Set ι := fun i => Set.Iic i.
theorem
ProbabilityTheory.indep_biSup_limsup
{Ω : Type u_1}
{ι : Type u_2}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{s : ι → MeasurableSpace Ω}
{p : Set ι → Prop}
{f : Filter ι}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.iIndep s)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
{t : Set ι}
(ht : p t)
:
ProbabilityTheory.Indep (⨆ (n : ι) (_ : n ∈ t), s n) (Filter.limsup s f)
theorem
ProbabilityTheory.indep_iSup_directed_limsup
{Ω : Type u_1}
{ι : Type u_2}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{s : ι → MeasurableSpace Ω}
{α : Type u_3}
{p : Set ι → Prop}
{f : Filter ι}
{ns : α → Set ι}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.iIndep s)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
(hns : Directed (fun x x_1 => x ≤ x_1) ns)
(hnsp : (a : α) → p (ns a))
:
ProbabilityTheory.Indep (⨆ (a : α) (n : ι) (_ : n ∈ ns a), s n) (Filter.limsup s f)
theorem
ProbabilityTheory.indep_iSup_limsup
{Ω : Type u_1}
{ι : Type u_2}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{s : ι → MeasurableSpace Ω}
{α : Type u_3}
{p : Set ι → Prop}
{f : Filter ι}
{ns : α → Set ι}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.iIndep s)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
(hns : Directed (fun x x_1 => x ≤ x_1) ns)
(hnsp : (a : α) → p (ns a))
(hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a)
:
ProbabilityTheory.Indep (⨆ (n : ι), s n) (Filter.limsup s f)
theorem
ProbabilityTheory.indep_limsup_self
{Ω : Type u_1}
{ι : Type u_2}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{s : ι → MeasurableSpace Ω}
{α : Type u_3}
{p : Set ι → Prop}
{f : Filter ι}
{ns : α → Set ι}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.iIndep s)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
(hns : Directed (fun x x_1 => x ≤ x_1) ns)
(hnsp : (a : α) → p (ns a))
(hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a)
:
ProbabilityTheory.Indep (Filter.limsup s f) (Filter.limsup s f)
theorem
ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup
{Ω : Type u_1}
{ι : Type u_2}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{s : ι → MeasurableSpace Ω}
{α : Type u_3}
{p : Set ι → Prop}
{f : Filter ι}
{ns : α → Set ι}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.iIndep s)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
(hns : Directed (fun x x_1 => x ≤ x_1) ns)
(hnsp : (a : α) → p (ns a))
(hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a)
{t : Set Ω}
(ht_tail : MeasurableSet t)
:
theorem
ProbabilityTheory.indep_limsup_atTop_self
{Ω : Type u_1}
{ι : Type u_2}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{s : ι → MeasurableSpace Ω}
[SemilatticeSup ι]
[NoMaxOrder ι]
[Nonempty ι]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.iIndep s)
:
ProbabilityTheory.Indep (Filter.limsup s Filter.atTop) (Filter.limsup s Filter.atTop)
theorem
ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atTop
{Ω : Type u_1}
{ι : Type u_2}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{s : ι → MeasurableSpace Ω}
[SemilatticeSup ι]
[NoMaxOrder ι]
[Nonempty ι]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.iIndep s)
{t : Set Ω}
(ht_tail : MeasurableSet t)
:
Kolmogorov's 0-1 law : any event in the tail σ-algebra of an independent sequence of
sub-σ-algebras has probability 0 or 1.
The tail σ-algebra limsup s atTop is the same as ⋂ n, ⋃ i ≥ n, s i.
theorem
ProbabilityTheory.indep_limsup_atBot_self
{Ω : Type u_1}
{ι : Type u_2}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{s : ι → MeasurableSpace Ω}
[SemilatticeInf ι]
[NoMinOrder ι]
[Nonempty ι]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.iIndep s)
:
ProbabilityTheory.Indep (Filter.limsup s Filter.atBot) (Filter.limsup s Filter.atBot)
theorem
ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atBot
{Ω : Type u_1}
{ι : Type u_2}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{s : ι → MeasurableSpace Ω}
[SemilatticeInf ι]
[NoMinOrder ι]
[Nonempty ι]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.iIndep s)
{t : Set Ω}
(ht_tail : MeasurableSet t)
:
Kolmogorov's 0-1 law : any event in the tail σ-algebra of an independent sequence of sub-σ-algebras has probability 0 or 1.