condExp_zero_or_one_of_measurableSet_limsup_atTop

English

A variant stating that under similar hypotheses, the conditional tail events have conditional probability 0 or 1 almost surely.

Русский

Вариант утверждения: при сходных гипотезах хвостовые события имеют условную вероятность 0 или 1 почти surely.

LaTeX

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

Lean4

theorem condExp_zero_or_one_of_measurableSet_limsup_atTop [StandardBorelSpace Ω] (hm : m ≤ m0) [IsFiniteMeasure μ]
    (h_le : ∀ n, s n ≤ m0) (h_indep : iCondIndep m hm s μ) {t : Set Ω} (ht_tail : MeasurableSet[limsup s atTop] 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_atTop_self hm h_le h_indep).condIndepSet_of_measurableSet ht_tail ht_tail)

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