English
Let a standard Borel (Ω) space be given with sigma-algebras m ≤ m0, and a family s of sub-sigma-algebras which is conditionally independent in the sense iCondIndep relative to m and hm. Given a tail construction with a directed ns and a witness function n ↦ a, the limsup sigma-algebras limsup s f are conditionally independent from themselves with respect to hm and μ.
Русский
Пусть имеется пространство (Ω) стандартного борелевского типа с сигм-алгебрами m ⊆ m0, семейство s подп_SIG-алгебр, которые условно независимы в смысле iCondIndep относительно m и hm. При задании хвостовой конструкции ns и фиксатора n ↦ a, предельные сигма-алгебры limsup s f являются условно независимыми сами от себя по отношению ко hm и μ.
LaTeX
$$$\text{CondIndep}\; m\; (\limsup s f)\; (\limsup s f)\; hm\ μ$$$
Lean4
theorem condIndep_limsup_self [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) : CondIndep m (limsup s f) (limsup s f) hm μ :=
Kernel.indep_limsup_self h_le h_indep hf hns hnsp hns_univ
