English
Under iCondIndep and standard assumptions, for ht_tail tail-measurable t, almost surely the conditional exp of t equals 0 or 1.
Русский
При iCondIndep и стандартных предположениях, для ht_tail хвостового измеримого t условное ожидание принимает 0 или 1 почти наверняка.
LaTeX
$$$\forall {t}, ht\_tail \Rightarrow (\text{condExp } m μ\; (t.indicator) )\in \{0,1\} \text{ a.e.}$$$
Lean4
/-- **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. -/
theorem condExp_zero_or_one_of_measurableSet_limsup_atBot [StandardBorelSpace Ω] (hm : m ≤ m0) [IsFiniteMeasure μ]
(h_le : ∀ n, s n ≤ m0) (h_indep : iCondIndep m hm s μ) {t : Set Ω} (ht_tail : MeasurableSet[limsup s atBot] t) :
∀ᵐ ω ∂μ, (μ⟦t|m⟧) ω = 0 ∨ (μ⟦t|m⟧) ω = 1 :=
condExp_eq_zero_or_one_of_condIndepSet_self hm (limsup_le_iSup.trans (iSup_le h_le) t ht_tail)
((condIndep_limsup_atBot_self hm h_le h_indep).condIndepSet_of_measurableSet ht_tail ht_tail)
