English
The kernel version asserts the same tail 0-1 behavior, but in the setting of a Markov kernel κ and finite measure μ on Ω with a family s of sub-sigma-algebras. For any tail measurable t, either κ a t = 0 or κ a t = 1 for μ-a.e. a.
Русский
Версия для ядра утверждает тот же хвостовой закон 0-1 для ядра Маркова κ и меры μ; для любого хвостового измеримого множества t верно, что κ a t равно 0 или 1 почти везде по a.
LaTeX
$$$\forall t\, (t\in\text{Tail}(s,f))\; (κ a t) \in \{0,1\} \text{ для почти всех } a$$
Lean4
theorem measure_zero_or_one_of_measurableSet_limsup (h_le : ∀ n, s n ≤ m0) (h_indep : iIndep 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 = 0 ∨ μ t = 1 := by
simpa only [ae_dirac_eq, Filter.eventually_pure] using
Kernel.measure_zero_or_one_of_measurableSet_limsup h_le h_indep hf hns hnsp hns_univ ht_tail
