theorem tailMeasurableSpace_eq_limsup_atTop {Ω : Type u_1} (𝓐 : ℕ → MeasurableSpace Ω) : tailMeasurableSpace 𝓐 = Filter.limsup 𝓐 Filter.atTop

The tail σ-algebra ⋂ₙ σ(𝓐 n, 𝓐 (n+1), …) coincides with limsup of the sequence of σ-algebras along atTop.

theorem kolmogorov_zero_one {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (𝓐 : ℕ → MeasurableSpace Ω) (h_le : ∀ (n : ℕ), 𝓐 n ≤ m0) (h_indep : ProbabilityTheory.iIndep 𝓐 μ) {A : Set Ω} (hA : MeasurableSet A) : μ A = 0 ∨ μ A = 1

Kolmogorov 0-1 law (for independent σ-algebras). If 𝓐 : ℕ → MeasurableSpace Ω is a sequence of independent sub-σ-algebras of m0, then every event A in the tail σ-algebra ⋂ₙ σ(𝓐 n, 𝓐 (n+1), …) satisfies μ A = 0 or μ A = 1.

theorem kolmogorov_zero_one_fun {Ω : Type u_1} {β : Type u_2} [mβ : MeasurableSpace β] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (X : ℕ → Ω → β) (h_le : ∀ (n : ℕ), MeasurableSpace.comap (X n) mβ ≤ m0) (h_indep : ProbabilityTheory.iIndep (fun (n : ℕ) => MeasurableSpace.comap (X n) mβ) μ) {A : Set Ω} (hA : MeasurableSet A) : μ A = 0 ∨ μ A = 1

Kolmogorov 0-1 law (for sequences of random variables). If X : ℕ → Ω → β is a sequence of random variables whose generated σ-algebras are independent, then every event A in the tail σ-algebra ⋂ₙ σ(X n, X (n+1), …) satisfies μ A = 0 or μ A = 1.

theorem kolmogorov_zero_one_of_iIndepFun {Ω : Type u_1} {β : Type u_2} [mβ : MeasurableSpace β] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (X : ℕ → Ω → β) (h_le : ∀ (n : ℕ), MeasurableSpace.comap (X n) mβ ≤ m0) (h_indep : ProbabilityTheory.iIndepFun X μ) {A : Set Ω} (hA : MeasurableSet A) : μ A = 0 ∨ μ A = 1

Kolmogorov 0-1 law from iIndepFun. If X : ℕ → Ω → β is an independent sequence of random variables (in the iIndepFun sense), then every event A in the tail σ-algebra of X satisfies μ A = 0 or μ A = 1.