# Documentation

Mathlib.Probability.Independence.ZeroOne

# 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 σ-algebra limsup s atTop of an independent sequence of σ-algebras s has probability 0 or 1.
theorem ProbabilityTheory.measure_eq_zero_or_one_or_top_of_indepSet_self {Ω : Type u_1} {m0 : } {μ : } {t : Set Ω} (h_indep : ) :
μ t = 0 μ t = 1 μ t =
theorem ProbabilityTheory.measure_eq_zero_or_one_of_indepSetCat_self {Ω : Type u_1} {m0 : } {μ : } {t : Set Ω} (h_indep : ) :
μ t = 0 μ t = 1
theorem ProbabilityTheory.indep_biSup_compl {Ω : Type u_1} {ι : Type u_2} {m0 : } {μ : } {s : ι} (h_le : ∀ (n : ι), s n m0) (h_indep : ) (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 ι → 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 = 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 : } {μ : } {s : ι} {p : Set ιProp} {f : } (h_le : ∀ (n : ι), s n m0) (h_indep : ) (hf : ∀ (t : Set ι), p tt f) {t : Set ι} (ht : p t) :
ProbabilityTheory.Indep (⨆ (n : ι) (_ : n t), s n) ()
theorem ProbabilityTheory.indep_iSup_directed_limsup {Ω : Type u_1} {ι : Type u_2} {m0 : } {μ : } {s : ι} {α : Type u_3} {p : Set ιProp} {f : } {ns : αSet ι} (h_le : ∀ (n : ι), s n m0) (h_indep : ) (hf : ∀ (t : Set ι), p tt 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) ()
theorem ProbabilityTheory.indep_iSup_limsup {Ω : Type u_1} {ι : Type u_2} {m0 : } {μ : } {s : ι} {α : Type u_3} {p : Set ιProp} {f : } {ns : αSet ι} (h_le : ∀ (n : ι), s n m0) (h_indep : ) (hf : ∀ (t : Set ι), p tt 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) ()
theorem ProbabilityTheory.indep_limsup_self {Ω : Type u_1} {ι : Type u_2} {m0 : } {μ : } {s : ι} {α : Type u_3} {p : Set ιProp} {f : } {ns : αSet ι} (h_le : ∀ (n : ι), s n m0) (h_indep : ) (hf : ∀ (t : Set ι), p tt f) (hns : Directed (fun x x_1 => x x_1) ns) (hnsp : (a : α) → p (ns a)) (hns_univ : ∀ (n : ι), a, n ns a) :
theorem ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup {Ω : Type u_1} {ι : Type u_2} {m0 : } {μ : } {s : ι} {α : Type u_3} {p : Set ιProp} {f : } {ns : αSet ι} (h_le : ∀ (n : ι), s n m0) (h_indep : ) (hf : ∀ (t : Set ι), p tt 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 : ) :
μ t = 0 μ t = 1
theorem ProbabilityTheory.indep_limsup_atTop_self {Ω : Type u_1} {ι : Type u_2} {m0 : } {μ : } {s : ι} [] [] [] (h_le : ∀ (n : ι), s n m0) (h_indep : ) :
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 : } {μ : } {s : ι} [] [] [] (h_le : ∀ (n : ι), s n m0) (h_indep : ) {t : Set Ω} (ht_tail : ) :
μ 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 atTop is the same as ⋂ n, ⋃ i ≥ n, s i.

theorem ProbabilityTheory.indep_limsup_atBot_self {Ω : Type u_1} {ι : Type u_2} {m0 : } {μ : } {s : ι} [] [] [] (h_le : ∀ (n : ι), s n m0) (h_indep : ) :
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 : } {μ : } {s : ι} [] [] [] (h_le : ∀ (n : ι), s n m0) (h_indep : ) {t : Set Ω} (ht_tail : ) :
μ 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.