condIndep_iSup_directed_limsup — Mathlib

English

If the family is conditionally independent and the index-directed structure holds, then the CondIndep between iSup s and limsup s f follows.

Русский

Если семейство условно независимо и структура индексов ориентирована, то следует CondIndep между iSup s и limsup s f.

LaTeX

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

Lean4

theorem condIndep_iSup_directed_limsup [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)) :
    CondIndep m (⨆ a, ⨆ n ∈ ns a, s n) (limsup s f) hm μ :=
  Kernel.indep_iSup_directed_limsup h_le h_indep hf hns hnsp

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