# mathlib3documentation

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 #

• 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 σ-algebra limsup s at_top of an independent sequence of σ-algebras s has 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 : μ) :
μ t = 0 μ t = 1 μ t =
theorem probability_theory.measure_eq_zero_or_one_of_indep_set_self {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {t : set Ω} (h_indep : μ) :
μ t = 0 μ t = 1
theorem probability_theory.indep_bsupr_compl {Ω : Type u_1} {ι : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {s : ι } (h_le : (n : ι), s n m0) (h_indep : μ) (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:

• p : set ι → Prop such that for a set t, p t → tᶜ ∈ f,
• ns : α → set ι a directed sequence of sets which all verify p and 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 Ω} {s : ι } {p : set ι Prop} {f : filter ι} (h_le : (n : ι), s n m0) (h_indep : μ) (hf : (t : set ι), p t t f) {t : set ι} (ht : p t) :
probability_theory.indep ( (n : ι) (H : n t), s n) f) μ
theorem probability_theory.indep_supr_directed_limsup {Ω : Type u_1} {ι : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {s : ι } {α : Type u_3} {p : set ι Prop} {f : filter ι} {ns : α set ι} (h_le : (n : ι), s n m0) (h_indep : μ) (hf : (t : set ι), p t t f) (hns : ns) (hnsp : (a : α), p (ns a)) :
probability_theory.indep ( (a : α) (n : ι) (H : n ns a), s n) f) μ
theorem probability_theory.indep_supr_limsup {Ω : Type u_1} {ι : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {s : ι } {α : Type u_3} {p : set ι Prop} {f : filter ι} {ns : α set ι} (h_le : (n : ι), s n m0) (h_indep : μ) (hf : (t : set ι), p t t f) (hns : ns) (hnsp : (a : α), p (ns a)) (hns_univ : (n : ι), (a : α), n ns a) :
probability_theory.indep ( (n : ι), s n) f) μ
theorem probability_theory.indep_limsup_self {Ω : Type u_1} {ι : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {s : ι } {α : Type u_3} {p : set ι Prop} {f : filter ι} {ns : α set ι} (h_le : (n : ι), s n m0) (h_indep : μ) (hf : (t : set ι), p t t f) (hns : ns) (hnsp : (a : α), p (ns a)) (hns_univ : (n : ι), (a : α), n ns a) :
f) μ
theorem probability_theory.measure_zero_or_one_of_measurable_set_limsup {Ω : Type u_1} {ι : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {s : ι } {α : Type u_3} {p : set ι Prop} {f : filter ι} {ns : α set ι} (h_le : (n : ι), s n m0) (h_indep : μ) (hf : (t : set ι), p t t f) (hns : 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.indep_limsup_at_top_self {Ω : Type u_1} {ι : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {s : ι } [no_max_order ι] [nonempty ι] (h_le : (n : ι), s n m0) (h_indep : μ) :
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 Ω} {s : ι } [no_max_order ι] [nonempty ι] (h_le : (n : ι), s n m0) (h_indep : μ) {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.indep_limsup_at_bot_self {Ω : Type u_1} {ι : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {s : ι } [no_min_order ι] [nonempty ι] (h_le : (n : ι), s n m0) (h_indep : μ) :
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 Ω} {s : ι } [no_min_order ι] [nonempty ι] (h_le : (n : ι), s n m0) (h_indep : μ) {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.