measure_zero_or_one_of_measurableSet_limsup_atBot

English

Kolmogorov’s 0-1 law for tail behavior: tail events measured by limsup s atTop have probability 0 or 1 under the independent sequence {s_n}.

Русский

Колмогоровский закон 0-1 для хвостового поведения: хвостовые события, измеряемые лимсапом limsup s atTop, имеют вероятность 0 или 1 для независимой последовательности {s_n}.

LaTeX

$$$\mu(t) \in \{0,1\}$ for all tail measurable t$$

Lean4

/-- **Kolmogorov's 0-1 law** : any event in the tail σ-algebra of an independent sequence of
sub-σ-algebras has probability 0 or 1. -/
theorem measure_zero_or_one_of_measurableSet_limsup_atBot (h_le : ∀ n, s n ≤ m0) (h_indep : iIndep s μ) {t : Set Ω}
    (ht_tail : MeasurableSet[limsup s atBot] t) : μ t = 0 ∨ μ t = 1 := by
  simpa only [ae_dirac_eq, Filter.eventually_pure] using
    Kernel.measure_zero_or_one_of_measurableSet_limsup_atBot h_le h_indep ht_tail

Похожие утверждения