# 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.

source
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 = ⊤
source
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 = ⊤
source
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
source
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
source
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
source
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
source
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) κ μα
source
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) μ
source
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`.

source
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) κ μα
source
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) μ
source
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 μ
source
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) κ μα
source
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) μ
source
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 μ
source
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) κ μα
source
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) μ
source
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 μ
source
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) κ μα
source
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) μ
source
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 μ
source
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
source
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
source
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
source
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) κ μα
source
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) μ
source
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 μ
source
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
source
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`.

source
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
source
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) κ μα
source
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) μ
source
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 μ
source
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.

source
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.

source
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.