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 #

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

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 Ω} {κ : ProbabilityTheory.Kernel α Ω} {μα : MeasureTheory.Measure α} {p : Set ιProp} {f : Filter ι} (h_le : ∀ (n : ι), s n m0) (h_indep : ProbabilityTheory.Kernel.iIndep s κ μα) (hf : ∀ (t : Set ι), p tt f) {t : Set ι} (ht : p t) :
ProbabilityTheory.Kernel.Indep (⨆ nt, 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 : ProbabilityTheory.iIndep s μ) (hf : ∀ (t : Set ι), p tt f) {t : Set ι} (ht : p t) :
ProbabilityTheory.Indep (⨆ nt, s n) (Filter.limsup s f) μ
theorem ProbabilityTheory.condIndep_biSup_limsup {Ω : Type u_2} {ι : Type u_3} {s : ιMeasurableSpace Ω} {m : MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {p : Set ιProp} {f : Filter ι} [StandardBorelSpace Ω] (hm : m m0) [MeasureTheory.IsFiniteMeasure μ] (h_le : ∀ (n : ι), s n m0) (h_indep : ProbabilityTheory.iCondIndep m hm s μ) (hf : ∀ (t : Set ι), p tt f) {t : Set ι} (ht : p t) :
ProbabilityTheory.CondIndep m (⨆ nt, 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 Ω} {κ : ProbabilityTheory.Kernel α Ω} {μα : MeasureTheory.Measure α} {β : Type u_4} {p : Set ιProp} {f : Filter ι} {ns : βSet ι} (h_le : ∀ (n : ι), s n m0) (h_indep : ProbabilityTheory.Kernel.iIndep s κ μα) (hf : ∀ (t : Set ι), p tt f) (hns : Directed (fun (x1 x2 : Set ι) => x1 x2) ns) (hnsp : ∀ (a : β), p (ns a)) :
ProbabilityTheory.Kernel.Indep (⨆ (a : β), nns 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 : ProbabilityTheory.iIndep s μ) (hf : ∀ (t : Set ι), p tt f) (hns : Directed (fun (x1 x2 : Set ι) => x1 x2) ns) (hnsp : ∀ (a : β), p (ns a)) :
ProbabilityTheory.Indep (⨆ (a : β), nns a, s n) (Filter.limsup s f) μ
theorem ProbabilityTheory.condIndep_iSup_directed_limsup {Ω : Type u_2} {ι : Type u_3} {s : ιMeasurableSpace Ω} {m : MeasurableSpace Ω} {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 : ProbabilityTheory.iCondIndep m hm s μ) (hf : ∀ (t : Set ι), p tt f) (hns : Directed (fun (x1 x2 : Set ι) => x1 x2) ns) (hnsp : ∀ (a : β), p (ns a)) :
ProbabilityTheory.CondIndep m (⨆ (a : β), nns 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 Ω} {κ : ProbabilityTheory.Kernel α Ω} {μα : MeasureTheory.Measure α} {β : Type u_4} {p : Set ιProp} {f : Filter ι} {ns : βSet ι} (h_le : ∀ (n : ι), s n m0) (h_indep : ProbabilityTheory.Kernel.iIndep s κ μα) (hf : ∀ (t : Set ι), p tt f) (hns : Directed (fun (x1 x2 : Set ι) => x1 x2) ns) (hnsp : ∀ (a : β), p (ns a)) (hns_univ : ∀ (n : ι), ∃ (a : β), n ns a) :
ProbabilityTheory.Kernel.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 : ProbabilityTheory.iIndep s μ) (hf : ∀ (t : Set ι), p tt f) (hns : Directed (fun (x1 x2 : Set ι) => x1 x2) ns) (hnsp : ∀ (a : β), p (ns a)) (hns_univ : ∀ (n : ι), ∃ (a : β), n ns a) :
ProbabilityTheory.Indep (⨆ (n : ι), s n) (Filter.limsup s f) μ
theorem ProbabilityTheory.condIndep_iSup_limsup {Ω : Type u_2} {ι : Type u_3} {s : ιMeasurableSpace Ω} {m : MeasurableSpace Ω} {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 : ProbabilityTheory.iCondIndep m hm s μ) (hf : ∀ (t : Set ι), p tt f) (hns : Directed (fun (x1 x2 : Set ι) => x1 x2) ns) (hnsp : ∀ (a : β), p (ns a)) (hns_univ : ∀ (n : ι), ∃ (a : β), n ns a) :
ProbabilityTheory.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 Ω} {κ : ProbabilityTheory.Kernel α Ω} {μα : MeasureTheory.Measure α} {β : Type u_4} {p : Set ιProp} {f : Filter ι} {ns : βSet ι} (h_le : ∀ (n : ι), s n m0) (h_indep : ProbabilityTheory.Kernel.iIndep s κ μα) (hf : ∀ (t : Set ι), p tt f) (hns : Directed (fun (x1 x2 : Set ι) => x1 x2) ns) (hnsp : ∀ (a : β), p (ns a)) (hns_univ : ∀ (n : ι), ∃ (a : β), n ns a) :
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 : ProbabilityTheory.iIndep s μ) (hf : ∀ (t : Set ι), p tt f) (hns : Directed (fun (x1 x2 : Set ι) => x1 x2) ns) (hnsp : ∀ (a : β), p (ns a)) (hns_univ : ∀ (n : ι), ∃ (a : β), n ns a) :
theorem ProbabilityTheory.condIndep_limsup_self {Ω : Type u_2} {ι : Type u_3} {s : ιMeasurableSpace Ω} {m : MeasurableSpace Ω} {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 : ProbabilityTheory.iCondIndep m hm s μ) (hf : ∀ (t : Set ι), p tt f) (hns : Directed (fun (x1 x2 : Set ι) => x1 x2) 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α : MeasurableSpace α} {s : ιMeasurableSpace Ω} {m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μα : MeasureTheory.Measure α} {β : Type u_4} {p : Set ιProp} {f : Filter ι} {ns : βSet ι} (h_le : ∀ (n : ι), s n m0) (h_indep : ProbabilityTheory.Kernel.iIndep s κ μα) (hf : ∀ (t : Set ι), p tt 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 : ProbabilityTheory.iIndep s μ) (hf : ∀ (t : Set ι), p tt 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 : MeasurableSpace Ω} {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 : ProbabilityTheory.iCondIndep m hm s μ) (hf : ∀ (t : Set ι), p tt 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) :
∀ᵐ (ω : Ω) ∂μ, MeasureTheory.condexp m μ (t.indicator fun (ω : Ω) => 1) ω = 0 MeasureTheory.condexp m μ (t.indicator fun (ω : Ω) => 1) ω = 1
theorem ProbabilityTheory.Kernel.indep_limsup_atTop_self {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ιMeasurableSpace Ω} {m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μα : MeasureTheory.Measure α} [SemilatticeSup ι] [NoMaxOrder ι] [Nonempty ι] (h_le : ∀ (n : ι), s n m0) (h_indep : ProbabilityTheory.Kernel.iIndep s κ μα) :
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} {s : ιMeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [SemilatticeSup ι] [NoMaxOrder ι] [Nonempty ι] (h_le : ∀ (n : ι), s n m0) (h_indep : ProbabilityTheory.iIndep s μ) :
ProbabilityTheory.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 : MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [SemilatticeSup ι] [NoMaxOrder ι] [Nonempty ι] [StandardBorelSpace Ω] (hm : m m0) [MeasureTheory.IsFiniteMeasure μ] (h_le : ∀ (n : ι), s n m0) (h_indep : ProbabilityTheory.iCondIndep m hm s μ) :
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α : MeasurableSpace α} {s : ιMeasurableSpace Ω} {m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μα : MeasureTheory.Measure α} [SemilatticeSup ι] [NoMaxOrder ι] [Nonempty ι] (h_le : ∀ (n : ι), s n m0) (h_indep : ProbabilityTheory.Kernel.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 : ProbabilityTheory.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 : MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [SemilatticeSup ι] [NoMaxOrder ι] [Nonempty ι] [StandardBorelSpace Ω] (hm : m m0) [MeasureTheory.IsFiniteMeasure μ] (h_le : ∀ (n : ι), s n m0) (h_indep : ProbabilityTheory.iCondIndep m hm s μ) {t : Set Ω} (ht_tail : MeasurableSet t) :
∀ᵐ (ω : Ω) ∂μ, MeasureTheory.condexp m μ (t.indicator fun (ω : Ω) => 1) ω = 0 MeasureTheory.condexp m μ (t.indicator fun (ω : Ω) => 1) ω = 1
theorem ProbabilityTheory.Kernel.indep_limsup_atBot_self {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ιMeasurableSpace Ω} {m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μα : MeasureTheory.Measure α} [SemilatticeInf ι] [NoMinOrder ι] [Nonempty ι] (h_le : ∀ (n : ι), s n m0) (h_indep : ProbabilityTheory.Kernel.iIndep s κ μα) :
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} {s : ιMeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [SemilatticeInf ι] [NoMinOrder ι] [Nonempty ι] (h_le : ∀ (n : ι), s n m0) (h_indep : ProbabilityTheory.iIndep s μ) :
ProbabilityTheory.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 : MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [SemilatticeInf ι] [NoMinOrder ι] [Nonempty ι] [StandardBorelSpace Ω] (hm : m m0) [MeasureTheory.IsFiniteMeasure μ] (h_le : ∀ (n : ι), s n m0) (h_indep : ProbabilityTheory.iCondIndep m hm s μ) :
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α : MeasurableSpace α} {s : ιMeasurableSpace Ω} {m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μα : MeasureTheory.Measure α} [SemilatticeInf ι] [NoMinOrder ι] [Nonempty ι] (h_le : ∀ (n : ι), s n m0) (h_indep : ProbabilityTheory.Kernel.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 : ProbabilityTheory.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 : MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [SemilatticeInf ι] [NoMinOrder ι] [Nonempty ι] [StandardBorelSpace Ω] (hm : m m0) [MeasureTheory.IsFiniteMeasure μ] (h_le : ∀ (n : ι), s n m0) (h_indep : ProbabilityTheory.iCondIndep m hm s μ) {t : Set Ω} (ht_tail : MeasurableSet t) :
∀ᵐ (ω : Ω) ∂μ, MeasureTheory.condexp m μ (t.indicator fun (ω : Ω) => 1) ω = 0 MeasureTheory.condexp m μ (t.indicator fun (ω : Ω) => 1) ω = 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.