measure_zero_or_one_of_measurableSet_limsup_atTop

English

Conditional version: under iCondIndep m hm s μ, for tail measurable t, the conditional expectation of its indicator is almost surely 0 or 1.

Русский

Условная версия: при iCondIndep m hm s μ вероятность хвоста превращается в 0-1 в условном ожидании: E[1_t|m] ∈ {0,1} почти surely.

LaTeX

$$$\forall t\; ht\; (E[1_{t}|m]\in\{0,1\})$ a.e.$$

Lean4

/-- **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 measure_zero_or_one_of_measurableSet_limsup_atTop (h_le : ∀ n, s n ≤ m0) (h_indep : iIndep s μ) {t : Set Ω}
    (ht_tail : MeasurableSet[limsup s atTop] t) : μ t = 0 ∨ μ t = 1 := by
  simpa only [ae_dirac_eq, Filter.eventually_pure] using
    Kernel.measure_zero_or_one_of_measurableSet_limsup_atTop h_le h_indep ht_tail

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