English
Let {s_n} be a directed family of sub-sigma-algebras of a measurable space Ω, contained in a fixed sigma-algebra m0, and let μ be a probability measure. Suppose the family is independent in the sense iIndep s μ, and that there exists a tail construction given by a filter f and a directed cover ns with the tail property. Then the limsup sigma-algebra limsup s f is independent of itself under μ, i.e. Indep(limsup s f, limsup s f) μ.
Русский
Пусть {s_n} — направленная семейство подпривад_sigma–алгебр пространства Ω, каждое из которых содержится в фиксированной сигма-алгебре m0, и есть мера μ. Предположим независимость в смысле iIndep s μ, а также существование хвостовой конструции через фильтр f и направленный набор ns, удовлетворяющей хвостовому свойству. Тогда хвостовая сигма-алгебра limsup s f независима сама от себя относительно μ: Indep(limsup s f, limsup s f) μ.
LaTeX
$$$\operatorname{Indep}\big(\limsup s f, \limsup s f\big)\,\mu$$$
Lean4
theorem indep_limsup_self (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) :
Indep (limsup s f) (limsup s f) μ :=
Kernel.indep_limsup_self h_le h_indep hf hns hnsp hns_univ
