English
Under a conditional independence regime iCondIndep m hm s μ, the conditional expectation over tail limsup s f behaves as a 0-1-valued conditional expectation on tail events.
Русский
При условной независимости iCondIndep m hm s μ условное ожидание хвостовых событий limsup s f принимает значения 0 или 1 на хвостовых множеств.
LaTeX
$$$\forall t\; (t\text{ tail})\; (E_{μ}(1_t | m)) \in \{0,1\}$$$
Lean4
theorem condExp_zero_or_one_of_measurableSet_limsup [StandardBorelSpace Ω] (hm : m ≤ m0) [IsFiniteMeasure μ]
(h_le : ∀ n, s n ≤ m0) (h_indep : iCondIndep m hm s μ) (hf : ∀ t, p t → tᶜ ∈ f) (hns : Directed (· ≤ ·) ns)
(hnsp : ∀ a, p (ns a)) (hns_univ : ∀ n, ∃ a, n ∈ ns a) {t : Set Ω} (ht_tail : MeasurableSet[limsup s f] t) :
∀ᵐ ω ∂μ, (μ⟦t|m⟧) ω = 0 ∨ (μ⟦t|m⟧) ω = 1 :=
by
have h :=
ae_of_ae_trim hm (Kernel.measure_zero_or_one_of_measurableSet_limsup h_le h_indep hf hns hnsp hns_univ ht_tail)
have ht : MeasurableSet t := limsup_le_iSup.trans (iSup_le h_le) t ht_tail
filter_upwards [condExpKernel_ae_eq_condExp hm ht, h] with ω hω_eq hω
rwa [← hω_eq, measureReal_eq_zero_iff, measureReal_def, ENNReal.toReal_eq_one_iff]
