condIndep_biSup_compl — Mathlib

English

Under conditional independence assumptions, the conditional independence between the combined sub-systems across a bipartition of indices extends to the limsup of the systems.

Русский

При условной независимости продолжим независимость между объединёнными подсистемами по биразделению индексов и limsup подсистем.

LaTeX

$$$\\text{CondIndep}\\left(m,\\,\\bigvee s_n,\\ limsup s f\\right)\\mu$$$

Lean4

theorem condIndep_biSup_compl [StandardBorelSpace Ω] (hm : m ≤ m0) [IsFiniteMeasure μ] (h_le : ∀ n, s n ≤ m0)
    (h_indep : iCondIndep m hm s μ) (t : Set ι) : CondIndep m (⨆ n ∈ t, s n) (⨆ n ∈ tᶜ, s n) hm μ :=
  Kernel.indep_biSup_compl h_le h_indep t

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