@[reducible]

def tailMeasurableSpaceFrom {Ω : Type u_1} (𝓐 : ℕ → MeasurableSpace Ω) (n : ℕ) : MeasurableSpace Ω

Given a sequence of σ-algebras 𝓐 i on Ω, tailMeasurableSpaceFrom 𝓐 n is the σ-algebra generated by 𝓐 i for all i ≥ n, i.e. σ(𝓐 n, 𝓐 (n+1), …).

@[reducible]

def tailMeasurableSpace {Ω : Type u_1} (𝓐 : ℕ → MeasurableSpace Ω) : MeasurableSpace Ω

The tail σ-algebra of a sequence of σ-algebras 𝓐 i, defined as 𝓣 = ⋂ₙ σ(𝓐 n, 𝓐 (n+1), …). It contains the information observable by looking only at events arbitrarily far into the future.

@[reducible, inline]

abbrev tailMeasurableSpaceOfFun {Ω : Type u_1} {β : Type u_2} [MeasurableSpace β] (X : ℕ → Ω → β) : MeasurableSpace Ω

The tail σ-algebra of a sequence of random variables X : ℕ → Ω → β, defined as 𝓣 = ⋂ₙ σ(X n, X (n+1), …). This is the standard tail σ-algebra appearing in Kolmogorov's 0-1 law.