condIndep_iSup_limsup — Mathlib

English

If all assumptions hold (StandardBorel, finite measure, measurability, etc.), then CondIndep between iSup and limsup along a directed index set follows.

Русский

Если соблюдены все предпосылки (StandardBorel, конечная мера, измеримость и т.д.), то CondIndep между iSup и limsup вдоль направленного множества индексов следует.

LaTeX

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

Lean4

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

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