Kolmogorov's 0-1 law #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Let s : ι → measurable_space Ω be an independent sequence of sub-σ-algebras. Then any set which
is measurable with respect to the tail σ-algebra limsup s at_top has probability 0 or 1.
Main statements #
measure_zero_or_one_of_measurable_set_limsup_at_top: Kolmogorov's 0-1 law. Any set which is measurable with respect to the tail σ-algebralimsup s at_topof an independent sequence of σ-algebrasshas probability 0 or 1.
theorem
probability_theory.measure_eq_zero_or_one_or_top_of_indep_set_self
{Ω : Type u_1}
{m0 : measurable_space Ω}
{μ : measure_theory.measure Ω}
{t : set Ω}
(h_indep : probability_theory.indep_set t t μ) :
theorem
probability_theory.measure_eq_zero_or_one_of_indep_set_self
{Ω : Type u_1}
{m0 : measurable_space Ω}
{μ : measure_theory.measure Ω}
[measure_theory.is_finite_measure μ]
{t : set Ω}
(h_indep : probability_theory.indep_set t t μ) :
theorem
probability_theory.indep_bsupr_compl
{Ω : Type u_1}
{ι : Type u_2}
{m0 : measurable_space Ω}
{μ : measure_theory.measure Ω}
[measure_theory.is_probability_measure μ]
{s : ι → measurable_space Ω}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : probability_theory.Indep s μ)
(t : set ι) :
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 = at_top, we can take p = bdd_above and ns : ι → set ι := λ i, set.Iic i.
theorem
probability_theory.indep_bsupr_limsup
{Ω : Type u_1}
{ι : Type u_2}
{m0 : measurable_space Ω}
{μ : measure_theory.measure Ω}
[measure_theory.is_probability_measure μ]
{s : ι → measurable_space Ω}
{p : set ι → Prop}
{f : filter ι}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : probability_theory.Indep s μ)
(hf : ∀ (t : set ι), p t → tᶜ ∈ f)
{t : set ι}
(ht : p t) :
probability_theory.indep (⨆ (n : ι) (H : n ∈ t), s n) (filter.limsup s f) μ
theorem
probability_theory.indep_supr_directed_limsup
{Ω : Type u_1}
{ι : Type u_2}
{m0 : measurable_space Ω}
{μ : measure_theory.measure Ω}
[measure_theory.is_probability_measure μ]
{s : ι → measurable_space Ω}
{α : Type u_3}
{p : set ι → Prop}
{f : filter ι}
{ns : α → set ι}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : probability_theory.Indep s μ)
(hf : ∀ (t : set ι), p t → tᶜ ∈ f)
(hns : directed has_le.le ns)
(hnsp : ∀ (a : α), p (ns a)) :
probability_theory.indep (⨆ (a : α) (n : ι) (H : n ∈ ns a), s n) (filter.limsup s f) μ
theorem
probability_theory.indep_supr_limsup
{Ω : Type u_1}
{ι : Type u_2}
{m0 : measurable_space Ω}
{μ : measure_theory.measure Ω}
[measure_theory.is_probability_measure μ]
{s : ι → measurable_space Ω}
{α : Type u_3}
{p : set ι → Prop}
{f : filter ι}
{ns : α → set ι}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : probability_theory.Indep s μ)
(hf : ∀ (t : set ι), p t → tᶜ ∈ f)
(hns : directed has_le.le ns)
(hnsp : ∀ (a : α), p (ns a))
(hns_univ : ∀ (n : ι), ∃ (a : α), n ∈ ns a) :
probability_theory.indep (⨆ (n : ι), s n) (filter.limsup s f) μ
theorem
probability_theory.indep_limsup_self
{Ω : Type u_1}
{ι : Type u_2}
{m0 : measurable_space Ω}
{μ : measure_theory.measure Ω}
[measure_theory.is_probability_measure μ]
{s : ι → measurable_space Ω}
{α : Type u_3}
{p : set ι → Prop}
{f : filter ι}
{ns : α → set ι}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : probability_theory.Indep s μ)
(hf : ∀ (t : set ι), p t → tᶜ ∈ f)
(hns : directed has_le.le ns)
(hnsp : ∀ (a : α), p (ns a))
(hns_univ : ∀ (n : ι), ∃ (a : α), n ∈ ns a) :
probability_theory.indep (filter.limsup s f) (filter.limsup s f) μ
theorem
probability_theory.measure_zero_or_one_of_measurable_set_limsup
{Ω : Type u_1}
{ι : Type u_2}
{m0 : measurable_space Ω}
{μ : measure_theory.measure Ω}
[measure_theory.is_probability_measure μ]
{s : ι → measurable_space Ω}
{α : Type u_3}
{p : set ι → Prop}
{f : filter ι}
{ns : α → set ι}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : probability_theory.Indep s μ)
(hf : ∀ (t : set ι), p t → tᶜ ∈ f)
(hns : directed has_le.le ns)
(hnsp : ∀ (a : α), p (ns a))
(hns_univ : ∀ (n : ι), ∃ (a : α), n ∈ ns a)
{t : set Ω}
(ht_tail : measurable_set t) :
theorem
probability_theory.indep_limsup_at_top_self
{Ω : Type u_1}
{ι : Type u_2}
{m0 : measurable_space Ω}
{μ : measure_theory.measure Ω}
[measure_theory.is_probability_measure μ]
{s : ι → measurable_space Ω}
[semilattice_sup ι]
[no_max_order ι]
[nonempty ι]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : probability_theory.Indep s μ) :
theorem
probability_theory.measure_zero_or_one_of_measurable_set_limsup_at_top
{Ω : Type u_1}
{ι : Type u_2}
{m0 : measurable_space Ω}
{μ : measure_theory.measure Ω}
[measure_theory.is_probability_measure μ]
{s : ι → measurable_space Ω}
[semilattice_sup ι]
[no_max_order ι]
[nonempty ι]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : probability_theory.Indep s μ)
{t : set Ω}
(ht_tail : measurable_set 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 at_top is the same as ⋂ n, ⋃ i ≥ n, s i.
theorem
probability_theory.indep_limsup_at_bot_self
{Ω : Type u_1}
{ι : Type u_2}
{m0 : measurable_space Ω}
{μ : measure_theory.measure Ω}
[measure_theory.is_probability_measure μ]
{s : ι → measurable_space Ω}
[semilattice_inf ι]
[no_min_order ι]
[nonempty ι]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : probability_theory.Indep s μ) :
theorem
probability_theory.measure_zero_or_one_of_measurable_set_limsup_at_bot
{Ω : Type u_1}
{ι : Type u_2}
{m0 : measurable_space Ω}
{μ : measure_theory.measure Ω}
[measure_theory.is_probability_measure μ]
{s : ι → measurable_space Ω}
[semilattice_inf ι]
[no_min_order ι]
[nonempty ι]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : probability_theory.Indep s μ)
{t : set Ω}
(ht_tail : measurable_set t) :
Kolmogorov's 0-1 law : any event in the tail σ-algebra of an independent sequence of sub-σ-algebras has probability 0 or 1.