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α : MeasurableSpace α} {m0 : MeasurableSpace Ω} {κ : Kernel α Ω} {μα : MeasureTheory.Measure α} {t : Set Ω} (h_indep : IndepSet t t κ μα) : ∀ᵐ (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 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : Set Ω} (h_indep : IndepSet t t μ) : μ t = 0 ∨ μ t = 1 ∨ μ t = ⊤

theorem ProbabilityTheory.Kernel.measure_eq_zero_or_one_of_indepSet_self' {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {m0 : MeasurableSpace Ω} {κ : Kernel α Ω} {μα : MeasureTheory.Measure α} (h : ∀ᵐ (a : α) ∂μα, MeasureTheory.IsFiniteMeasure (κ a)) {t : Set Ω} (h_indep : IndepSet t t κ μα) : ∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1

theorem ProbabilityTheory.Kernel.measure_eq_zero_or_one_of_indepSet_self {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {m0 : MeasurableSpace Ω} {κ : Kernel α Ω} {μα : MeasureTheory.Measure α} [h : ∀ (a : α), MeasureTheory.IsFiniteMeasure (κ a)] {t : Set Ω} (h_indep : IndepSet t t κ μα) : ∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1

theorem ProbabilityTheory.measure_eq_zero_or_one_of_indepSet_self {Ω : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {t : Set Ω} (h_indep : IndepSet t t μ) : μ t = 0 ∨ μ t = 1

theorem ProbabilityTheory.condExp_eq_zero_or_one_of_condIndepSet_self {Ω : Type u_2} {m m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [StandardBorelSpace Ω] (hm : m ≤ m0) [hμ : MeasureTheory.IsFiniteMeasure μ] {t : Set Ω} (ht : MeasurableSet t) (h_indep : CondIndepSet m hm t t μ) : ∀ᵐ (ω : Ω) ∂μ, μ[t.indicator fun (ω : Ω) => 1|m] ω = 0 ∨ μ[t.indicator fun (ω : Ω) => 1|m] ω = 1

theorem ProbabilityTheory.Kernel.indep_biSup_compl {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {κ : Kernel α Ω} {μα : MeasureTheory.Measure α} (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : iIndep s κ μα) (t : Set ι) : Indep (⨆ n ∈ t, s n) (⨆ n ∈ tᶜ, s n) κ μα

theorem ProbabilityTheory.indep_biSup_compl {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : iIndep s μ) (t : Set ι) : Indep (⨆ n ∈ t, s n) (⨆ n ∈ tᶜ, s n) μ

theorem ProbabilityTheory.condIndep_biSup_compl {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [StandardBorelSpace Ω] (hm : m ≤ m0) [MeasureTheory.IsFiniteMeasure μ] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : iCondIndep m hm s μ) (t : Set ι) : 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α : MeasurableSpace α} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {κ : Kernel α Ω} {μα : MeasureTheory.Measure α} {p : Set ι → Prop} {f : Filter ι} (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : iIndep s κ μα) (hf : ∀ (t : Set ι), p t → tᶜ ∈ f) {t : Set ι} (ht : p t) : Indep (⨆ n ∈ t, s n) (Filter.limsup s f) κ μα

theorem ProbabilityTheory.indep_biSup_limsup {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {p : Set ι → Prop} {f : Filter ι} (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : iIndep s μ) (hf : ∀ (t : Set ι), p t → tᶜ ∈ f) {t : Set ι} (ht : p t) : Indep (⨆ n ∈ t, s n) (Filter.limsup s f) μ

theorem ProbabilityTheory.condIndep_biSup_limsup {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {p : Set ι → Prop} {f : Filter ι} [StandardBorelSpace Ω] (hm : m ≤ m0) [MeasureTheory.IsFiniteMeasure μ] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : iCondIndep m hm s μ) (hf : ∀ (t : Set ι), p t → tᶜ ∈ f) {t : Set ι} (ht : p t) : CondIndep m (⨆ n ∈ t, s n) (Filter.limsup s f) hm μ

theorem ProbabilityTheory.Kernel.indep_iSup_directed_limsup {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {κ : Kernel α Ω} {μα : MeasureTheory.Measure α} {β : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι} (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : iIndep s κ μα) (hf : ∀ (t : Set ι), p t → tᶜ ∈ f) (hns : Directed (fun (x1 x2 : Set ι) => x1 ≤ x2) ns) (hnsp : ∀ (a : β), p (ns a)) : Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (Filter.limsup s f) κ μα

theorem ProbabilityTheory.indep_iSup_directed_limsup {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι} (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : iIndep s μ) (hf : ∀ (t : Set ι), p t → tᶜ ∈ f) (hns : Directed (fun (x1 x2 : Set ι) => x1 ≤ x2) ns) (hnsp : ∀ (a : β), p (ns a)) : Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (Filter.limsup s f) μ

theorem ProbabilityTheory.condIndep_iSup_directed_limsup {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι} [StandardBorelSpace Ω] (hm : m ≤ m0) [MeasureTheory.IsFiniteMeasure μ] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : iCondIndep m hm s μ) (hf : ∀ (t : Set ι), p t → tᶜ ∈ f) (hns : Directed (fun (x1 x2 : Set ι) => x1 ≤ x2) ns) (hnsp : ∀ (a : β), p (ns a)) : CondIndep m (⨆ (a : β), ⨆ n ∈ ns a, s n) (Filter.limsup s f) hm μ

theorem ProbabilityTheory.Kernel.indep_iSup_limsup {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {κ : Kernel α Ω} {μα : MeasureTheory.Measure α} {β : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι} (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : iIndep s κ μα) (hf : ∀ (t : Set ι), p t → tᶜ ∈ f) (hns : Directed (fun (x1 x2 : Set ι) => x1 ≤ x2) ns) (hnsp : ∀ (a : β), p (ns a)) (hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a) : Indep (⨆ (n : ι), s n) (Filter.limsup s f) κ μα

theorem ProbabilityTheory.indep_iSup_limsup {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι} (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : iIndep s μ) (hf : ∀ (t : Set ι), p t → tᶜ ∈ f) (hns : Directed (fun (x1 x2 : Set ι) => x1 ≤ x2) ns) (hnsp : ∀ (a : β), p (ns a)) (hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a) : Indep (⨆ (n : ι), s n) (Filter.limsup s f) μ

theorem ProbabilityTheory.condIndep_iSup_limsup {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι} [StandardBorelSpace Ω] (hm : m ≤ m0) [MeasureTheory.IsFiniteMeasure μ] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : iCondIndep m hm s μ) (hf : ∀ (t : Set ι), p t → tᶜ ∈ f) (hns : Directed (fun (x1 x2 : Set ι) => x1 ≤ x2) ns) (hnsp : ∀ (a : β), p (ns a)) (hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a) : CondIndep m (⨆ (n : ι), s n) (Filter.limsup s f) hm μ

theorem ProbabilityTheory.Kernel.indep_limsup_self {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {κ : Kernel α Ω} {μα : MeasureTheory.Measure α} {β : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι} (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : iIndep s κ μα) (hf : ∀ (t : Set ι), p t → tᶜ ∈ f) (hns : Directed (fun (x1 x2 : Set ι) => x1 ≤ x2) ns) (hnsp : ∀ (a : β), p (ns a)) (hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a) : Indep (Filter.limsup s f) (Filter.limsup s f) κ μα

theorem ProbabilityTheory.indep_limsup_self {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι} (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : iIndep s μ) (hf : ∀ (t : Set ι), p t → tᶜ ∈ f) (hns : Directed (fun (x1 x2 : Set ι) => x1 ≤ x2) ns) (hnsp : ∀ (a : β), p (ns a)) (hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a) : Indep (Filter.limsup s f) (Filter.limsup s f) μ

theorem ProbabilityTheory.condIndep_limsup_self {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι} [StandardBorelSpace Ω] (hm : m ≤ m0) [MeasureTheory.IsFiniteMeasure μ] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : iCondIndep m hm s μ) (hf : ∀ (t : Set ι), p t → tᶜ ∈ f) (hns : Directed (fun (x1 x2 : Set ι) => x1 ≤ x2) ns) (hnsp : ∀ (a : β), p (ns a)) (hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a) : CondIndep m (Filter.limsup s f) (Filter.limsup s f) hm μ

theorem ProbabilityTheory.Kernel.measure_zero_or_one_of_measurableSet_limsup {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {κ : Kernel α Ω} {μα : MeasureTheory.Measure α} {β : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι} (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : iIndep s κ μα) (hf : ∀ (t : Set ι), p t → tᶜ ∈ f) (hns : Directed (fun (x1 x2 : Set ι) => x1 ≤ x2) ns) (hnsp : ∀ (a : β), p (ns a)) (hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a) {t : Set Ω} (ht_tail : MeasurableSet t) : ∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1

theorem ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι} (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : iIndep s μ) (hf : ∀ (t : Set ι), p t → tᶜ ∈ f) (hns : Directed (fun (x1 x2 : Set ι) => x1 ≤ x2) ns) (hnsp : ∀ (a : β), p (ns a)) (hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a) {t : Set Ω} (ht_tail : MeasurableSet t) : μ t = 0 ∨ μ t = 1

theorem ProbabilityTheory.condExp_zero_or_one_of_measurableSet_limsup {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι} [StandardBorelSpace Ω] (hm : m ≤ m0) [MeasureTheory.IsFiniteMeasure μ] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : iCondIndep m hm s μ) (hf : ∀ (t : Set ι), p t → tᶜ ∈ f) (hns : Directed (fun (x1 x2 : Set ι) => x1 ≤ x2) ns) (hnsp : ∀ (a : β), p (ns a)) (hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a) {t : Set Ω} (ht_tail : MeasurableSet t) : ∀ᵐ (ω : Ω) ∂μ, μ[t.indicator fun (ω : Ω) => 1|m] ω = 0 ∨ μ[t.indicator fun (ω : Ω) => 1|m] ω = 1

theorem ProbabilityTheory.Kernel.indep_limsup_atTop_self {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {κ : Kernel α Ω} {μα : MeasureTheory.Measure α} [SemilatticeSup ι] [NoMaxOrder ι] [Nonempty ι] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : iIndep s κ μα) : Indep (Filter.limsup s Filter.atTop) (Filter.limsup s Filter.atTop) κ μα

theorem ProbabilityTheory.indep_limsup_atTop_self {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [SemilatticeSup ι] [NoMaxOrder ι] [Nonempty ι] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : iIndep s μ) : Indep (Filter.limsup s Filter.atTop) (Filter.limsup s Filter.atTop) μ

theorem ProbabilityTheory.condIndep_limsup_atTop_self {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [SemilatticeSup ι] [NoMaxOrder ι] [Nonempty ι] [StandardBorelSpace Ω] (hm : m ≤ m0) [MeasureTheory.IsFiniteMeasure μ] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : iCondIndep m hm s μ) : 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α : MeasurableSpace α} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {κ : Kernel α Ω} {μα : MeasureTheory.Measure α} [SemilatticeSup ι] [NoMaxOrder ι] [Nonempty ι] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : iIndep s κ μα) {t : Set Ω} (ht_tail : MeasurableSet t) : ∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1

theorem ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atTop {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [SemilatticeSup ι] [NoMaxOrder ι] [Nonempty ι] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : iIndep s μ) {t : Set Ω} (ht_tail : MeasurableSet 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 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} {s : ι → MeasurableSpace Ω} {m m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [SemilatticeSup ι] [NoMaxOrder ι] [Nonempty ι] [StandardBorelSpace Ω] (hm : m ≤ m0) [MeasureTheory.IsFiniteMeasure μ] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : iCondIndep m hm s μ) {t : Set Ω} (ht_tail : MeasurableSet t) : ∀ᵐ (ω : Ω) ∂μ, μ[t.indicator fun (ω : Ω) => 1|m] ω = 0 ∨ μ[t.indicator fun (ω : Ω) => 1|m] ω = 1

theorem ProbabilityTheory.Kernel.indep_limsup_atBot_self {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {κ : Kernel α Ω} {μα : MeasureTheory.Measure α} [SemilatticeInf ι] [NoMinOrder ι] [Nonempty ι] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : iIndep s κ μα) : Indep (Filter.limsup s Filter.atBot) (Filter.limsup s Filter.atBot) κ μα

theorem ProbabilityTheory.indep_limsup_atBot_self {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [SemilatticeInf ι] [NoMinOrder ι] [Nonempty ι] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : iIndep s μ) : Indep (Filter.limsup s Filter.atBot) (Filter.limsup s Filter.atBot) μ

theorem ProbabilityTheory.condIndep_limsup_atBot_self {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [SemilatticeInf ι] [NoMinOrder ι] [Nonempty ι] [StandardBorelSpace Ω] (hm : m ≤ m0) [MeasureTheory.IsFiniteMeasure μ] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : iCondIndep m hm s μ) : 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α : MeasurableSpace α} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {κ : Kernel α Ω} {μα : MeasureTheory.Measure α} [SemilatticeInf ι] [NoMinOrder ι] [Nonempty ι] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : iIndep s κ μα) {t : Set Ω} (ht_tail : MeasurableSet t) : ∀ᵐ (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} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [SemilatticeInf ι] [NoMinOrder ι] [Nonempty ι] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : iIndep s μ) {t : Set Ω} (ht_tail : MeasurableSet 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.

theorem ProbabilityTheory.condExp_zero_or_one_of_measurableSet_limsup_atBot {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [SemilatticeInf ι] [NoMinOrder ι] [Nonempty ι] [StandardBorelSpace Ω] (hm : m ≤ m0) [MeasureTheory.IsFiniteMeasure μ] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : iCondIndep m hm s μ) {t : Set Ω} (ht_tail : MeasurableSet t) : ∀ᵐ (ω : Ω) ∂μ, μ[t.indicator fun (ω : Ω) => 1|m] ω = 0 ∨ μ[t.indicator fun (ω : Ω) => 1|m] ω = 1

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