condIndep_biSup_limsup — Mathlib

English

Under appropriate measurability and standard space assumptions, iIndep together with directed ns implies indep between iSup s and limsup s f.

Русский

При надлежащей измеримости и стандартном пространстве iIndep вместе с направленным ns приводит к независимости между iSup s и limsup s f.

LaTeX

$$$\\text{Indep}\\left(\\iSup_{n} s_n, \\limsup s f\\right)\\mu$$$

Lean4

theorem condIndep_biSup_limsup [StandardBorelSpace Ω] (hm : m ≤ m0) [IsFiniteMeasure μ] (h_le : ∀ n, s n ≤ m0)
    (h_indep : iCondIndep m hm s μ) (hf : ∀ t, p t → tᶜ ∈ f) {t : Set ι} (ht : p t) :
    CondIndep m (⨆ n ∈ t, s n) (limsup s f) hm μ :=
  Kernel.indep_biSup_limsup h_le h_indep hf ht

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