mathlib3 documentation

probability.independence.zero_one

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 #

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 ι) :
probability_theory.indep ( (n : ι) (H : n t), s n) ( (n : ι) (H : 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:

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) :
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) :
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) :
μ t = 0 μ t = 1
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) :
μ t = 0 μ t = 1

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.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) :
μ t = 0 μ t = 1

Kolmogorov's 0-1 law : any event in the tail σ-algebra of an independent sequence of sub-σ-algebras has probability 0 or 1.