# 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.kernel.measure_eq_zero_or_one_or_top_of_indepSet_self {α : Type u_1} {Ω : Type u_2} {_mα : } {m0 : } {κ : ()} {μα : } {t : Set Ω} (h_indep : ) :
∀ᵐ (a : α) ∂μα, (κ a) t = 0 (κ a) t = 1 (κ a) t =
theorem ProbabilityTheory.measure_eq_zero_or_one_or_top_of_indepSet_self {Ω : Type u_2} {m0 : } {μ : } {t : Set Ω} (h_indep : ) :
μ t = 0 μ t = 1 μ t =
theorem ProbabilityTheory.kernel.measure_eq_zero_or_one_of_indepSet_self {α : Type u_1} {Ω : Type u_2} {_mα : } {m0 : } {κ : ()} {μα : } [∀ (a : α), ] {t : Set Ω} (h_indep : ) :
∀ᵐ (a : α) ∂μα, (κ a) t = 0 (κ a) t = 1
theorem ProbabilityTheory.measure_eq_zero_or_one_of_indepSet_self {Ω : Type u_2} {m0 : } {μ : } {t : Set Ω} (h_indep : ) :
μ t = 0 μ t = 1
theorem ProbabilityTheory.condexp_eq_zero_or_one_of_condIndepSet_self {Ω : Type u_2} {m : } {m0 : } {μ : } [] (hm : m m0) [hμ : ] {t : Set Ω} (ht : ) (h_indep : ) :
∀ᵐ (ω : Ω) ∂μ, MeasureTheory.condexp m μ (Set.indicator t fun (ω : Ω) => 1) ω = 0 MeasureTheory.condexp m μ (Set.indicator t fun (ω : Ω) => 1) ω = 1
theorem ProbabilityTheory.kernel.indep_biSup_compl {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {m0 : } {κ : ()} {μα : } {s : ι} (h_le : ∀ (n : ι), s n m0) (h_indep : ) (t : Set ι) :
ProbabilityTheory.kernel.Indep (⨆ n ∈ t, s n) (⨆ n ∈ t, s n) κ μα
theorem ProbabilityTheory.indep_biSup_compl {Ω : Type u_2} {ι : Type u_3} {m0 : } {μ : } {s : ι} (h_le : ∀ (n : ι), s n m0) (h_indep : ) (t : Set ι) :
ProbabilityTheory.Indep (⨆ n ∈ t, s n) (⨆ n ∈ t, s n) μ
theorem ProbabilityTheory.condIndep_biSup_compl {Ω : Type u_2} {ι : Type u_3} {m : } {m0 : } {μ : } {s : ι} [] (hm : m m0) (h_le : ∀ (n : ι), s n m0) (h_indep : ) (t : Set ι) :
ProbabilityTheory.CondIndep m (⨆ n ∈ t, s n) (⨆ n ∈ t, s n) hm μ

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.kernel.indep_biSup_limsup {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {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.kernel.Indep (⨆ n ∈ t, s n) () κ μα
theorem ProbabilityTheory.indep_biSup_limsup {Ω : Type u_2} {ι : Type u_3} {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 ∈ t, s n) () μ
theorem ProbabilityTheory.condIndep_biSup_limsup {Ω : Type u_2} {ι : Type u_3} {m : } {m0 : } {μ : } {s : ι} {p : Set ιProp} {f : } [] (hm : m m0) (h_le : ∀ (n : ι), s n m0) (h_indep : ) (hf : ∀ (t : Set ι), p tt f) {t : Set ι} (ht : p t) :
ProbabilityTheory.CondIndep m (⨆ n ∈ t, s n) () hm μ
theorem ProbabilityTheory.kernel.indep_iSup_directed_limsup {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {m0 : } {κ : ()} {μα : } {s : ι} {α : Type u_4} {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 : Set ι) => x x_1) ns) (hnsp : ∀ (a : α), p (ns a)) :
ProbabilityTheory.kernel.Indep (⨆ (a : α), ⨆ n ∈ ns a, s n) () κ μα
theorem ProbabilityTheory.indep_iSup_directed_limsup {Ω : Type u_2} {ι : Type u_3} {m0 : } {μ : } {s : ι} {α : Type u_4} {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 : Set ι) => x x_1) ns) (hnsp : ∀ (a : α), p (ns a)) :
ProbabilityTheory.Indep (⨆ (a : α), ⨆ n ∈ ns a, s n) () μ
theorem ProbabilityTheory.condIndep_iSup_directed_limsup {Ω : Type u_2} {ι : Type u_3} {m : } {m0 : } {μ : } {s : ι} {α : Type u_4} {p : Set ιProp} {f : } {ns : αSet ι} [] (hm : m m0) (h_le : ∀ (n : ι), s n m0) (h_indep : ) (hf : ∀ (t : Set ι), p tt f) (hns : Directed (fun (x x_1 : Set ι) => x x_1) ns) (hnsp : ∀ (a : α), p (ns a)) :
ProbabilityTheory.CondIndep m (⨆ (a : α), ⨆ n ∈ ns a, s n) () hm μ
theorem ProbabilityTheory.kernel.indep_iSup_limsup {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {m0 : } {κ : ()} {μα : } {s : ι} {α : Type u_4} {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 : Set ι) => x x_1) ns) (hnsp : ∀ (a : α), p (ns a)) (hns_univ : ∀ (n : ι), ∃ (a : α), n ns a) :
ProbabilityTheory.kernel.Indep (⨆ (n : ι), s n) () κ μα
theorem ProbabilityTheory.indep_iSup_limsup {Ω : Type u_2} {ι : Type u_3} {m0 : } {μ : } {s : ι} {α : Type u_4} {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 : Set ι) => x x_1) ns) (hnsp : ∀ (a : α), p (ns a)) (hns_univ : ∀ (n : ι), ∃ (a : α), n ns a) :
ProbabilityTheory.Indep (⨆ (n : ι), s n) () μ
theorem ProbabilityTheory.condIndep_iSup_limsup {Ω : Type u_2} {ι : Type u_3} {m : } {m0 : } {μ : } {s : ι} {α : Type u_4} {p : Set ιProp} {f : } {ns : αSet ι} [] (hm : m m0) (h_le : ∀ (n : ι), s n m0) (h_indep : ) (hf : ∀ (t : Set ι), p tt f) (hns : Directed (fun (x x_1 : Set ι) => x x_1) ns) (hnsp : ∀ (a : α), p (ns a)) (hns_univ : ∀ (n : ι), ∃ (a : α), n ns a) :
ProbabilityTheory.CondIndep m (⨆ (n : ι), s n) () hm μ
theorem ProbabilityTheory.kernel.indep_limsup_self {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {m0 : } {κ : ()} {μα : } {s : ι} {α : Type u_4} {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 : Set ι) => x x_1) ns) (hnsp : ∀ (a : α), p (ns a)) (hns_univ : ∀ (n : ι), ∃ (a : α), n ns a) :
theorem ProbabilityTheory.indep_limsup_self {Ω : Type u_2} {ι : Type u_3} {m0 : } {μ : } {s : ι} {α : Type u_4} {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 : Set ι) => x x_1) ns) (hnsp : ∀ (a : α), p (ns a)) (hns_univ : ∀ (n : ι), ∃ (a : α), n ns a) :
theorem ProbabilityTheory.condIndep_limsup_self {Ω : Type u_2} {ι : Type u_3} {m : } {m0 : } {μ : } {s : ι} {α : Type u_4} {p : Set ιProp} {f : } {ns : αSet ι} [] (hm : m m0) (h_le : ∀ (n : ι), s n m0) (h_indep : ) (hf : ∀ (t : Set ι), p tt f) (hns : Directed (fun (x x_1 : Set ι) => x x_1) ns) (hnsp : ∀ (a : α), p (ns a)) (hns_univ : ∀ (n : ι), ∃ (a : α), n ns a) :
theorem ProbabilityTheory.kernel.measure_zero_or_one_of_measurableSet_limsup {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {m0 : } {κ : ()} {μα : } {s : ι} {α : Type u_4} {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 : Set ι) => x x_1) ns) (hnsp : ∀ (a : α), p (ns a)) (hns_univ : ∀ (n : ι), ∃ (a : α), n ns a) {t : Set Ω} (ht_tail : ) :
∀ᵐ (a : α✝) ∂μα, (κ a) t = 0 (κ a) t = 1
theorem ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup {Ω : Type u_2} {ι : Type u_3} {m0 : } {μ : } {s : ι} {α : Type u_4} {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 : Set ι) => 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.condexp_zero_or_one_of_measurableSet_limsup {Ω : Type u_2} {ι : Type u_3} {m : } {m0 : } {μ : } {s : ι} {α : Type u_4} {p : Set ιProp} {f : } {ns : αSet ι} [] (hm : m m0) (h_le : ∀ (n : ι), s n m0) (h_indep : ) (hf : ∀ (t : Set ι), p tt f) (hns : Directed (fun (x x_1 : Set ι) => x x_1) ns) (hnsp : ∀ (a : α), p (ns a)) (hns_univ : ∀ (n : ι), ∃ (a : α), n ns a) {t : Set Ω} (ht_tail : ) :
∀ᵐ (ω : Ω) ∂μ, MeasureTheory.condexp m μ (Set.indicator t fun (ω : Ω) => 1) ω = 0 MeasureTheory.condexp m μ (Set.indicator t fun (ω : Ω) => 1) ω = 1
theorem ProbabilityTheory.kernel.indep_limsup_atTop_self {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {m0 : } {κ : ()} {μα : } {s : ι} [] [] [] (h_le : ∀ (n : ι), s n m0) (h_indep : ) :
ProbabilityTheory.kernel.Indep (Filter.limsup s Filter.atTop) (Filter.limsup s Filter.atTop) κ μα
theorem ProbabilityTheory.indep_limsup_atTop_self {Ω : Type u_2} {ι : Type u_3} {m0 : } {μ : } {s : ι} [] [] [] (h_le : ∀ (n : ι), s n m0) (h_indep : ) :
ProbabilityTheory.Indep (Filter.limsup s Filter.atTop) (Filter.limsup s Filter.atTop) μ
theorem ProbabilityTheory.condIndep_limsup_atTop_self {Ω : Type u_2} {ι : Type u_3} {m : } {m0 : } {μ : } {s : ι} [] [] [] [] (hm : m m0) (h_le : ∀ (n : ι), s n m0) (h_indep : ) :
ProbabilityTheory.CondIndep m (Filter.limsup s Filter.atTop) (Filter.limsup s Filter.atTop) hm μ
theorem ProbabilityTheory.kernel.measure_zero_or_one_of_measurableSet_limsup_atTop {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {m0 : } {κ : ()} {μα : } {s : ι} [] [] [] (h_le : ∀ (n : ι), s n m0) (h_indep : ) {t : Set Ω} (ht_tail : ) :
∀ᵐ (a : α) ∂μα, (κ a) t = 0 (κ a) t = 1
theorem ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atTop {Ω : Type u_2} {ι : Type u_3} {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.condexp_zero_or_one_of_measurableSet_limsup_atTop {Ω : Type u_2} {ι : Type u_3} {m : } {m0 : } {μ : } {s : ι} [] [] [] [] (hm : m m0) (h_le : ∀ (n : ι), s n m0) (h_indep : ) {t : Set Ω} (ht_tail : ) :
∀ᵐ (ω : Ω) ∂μ, MeasureTheory.condexp m μ (Set.indicator t fun (ω : Ω) => 1) ω = 0 MeasureTheory.condexp m μ (Set.indicator t fun (ω : Ω) => 1) ω = 1
theorem ProbabilityTheory.kernel.indep_limsup_atBot_self {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {m0 : } {κ : ()} {μα : } {s : ι} [] [] [] (h_le : ∀ (n : ι), s n m0) (h_indep : ) :
ProbabilityTheory.kernel.Indep (Filter.limsup s Filter.atBot) (Filter.limsup s Filter.atBot) κ μα
theorem ProbabilityTheory.indep_limsup_atBot_self {Ω : Type u_2} {ι : Type u_3} {m0 : } {μ : } {s : ι} [] [] [] (h_le : ∀ (n : ι), s n m0) (h_indep : ) :
ProbabilityTheory.Indep (Filter.limsup s Filter.atBot) (Filter.limsup s Filter.atBot) μ
theorem ProbabilityTheory.condIndep_limsup_atBot_self {Ω : Type u_2} {ι : Type u_3} {m : } {m0 : } {μ : } {s : ι} [] [] [] [] (hm : m m0) (h_le : ∀ (n : ι), s n m0) (h_indep : ) :
ProbabilityTheory.CondIndep m (Filter.limsup s Filter.atBot) (Filter.limsup s Filter.atBot) hm μ
theorem ProbabilityTheory.kernel.measure_zero_or_one_of_measurableSet_limsup_atBot {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {m0 : } {κ : ()} {μα : } {s : ι} [] [] [] (h_le : ∀ (n : ι), s n m0) (h_indep : ) {t : Set Ω} (ht_tail : ) :
∀ᵐ (a : α) ∂μα, (κ a) t = 0 (κ a) t = 1

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

theorem ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atBot {Ω : Type u_2} {ι : Type u_3} {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.

theorem ProbabilityTheory.condexp_zero_or_one_of_measurableSet_limsup_atBot {Ω : Type u_2} {ι : Type u_3} {m : } {m0 : } {μ : } {s : ι} [] [] [] [] (hm : m m0) (h_le : ∀ (n : ι), s n m0) (h_indep : ) {t : Set Ω} (ht_tail : ) :
∀ᵐ (ω : Ω) ∂μ, MeasureTheory.condexp m μ (Set.indicator t fun (ω : Ω) => 1) ω = 0 MeasureTheory.condexp m μ (Set.indicator t fun (ω : Ω) => 1) ω = 1

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