indep_iSup_limsup — Mathlib

English

Under standard assumptions, the independence between iSup s and limsup s f holds with a directed ns and a nonempty condition.

Русский

При стандартных предположениях независимость между iSup s и limsup s f сохраняется при направленном ns и не пустом условии.

LaTeX

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

Lean4

theorem indep_iSup_limsup (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 (⨆ n, s n) (limsup s f) μ :=
  Kernel.indep_iSup_limsup h_le h_indep hf hns hnsp hns_univ

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