indep_biSup_limsup — Mathlib

English

If the family s_n is increasing and independent in the iIndep sense, then the iSup over a directed index set and the limsup along a filter are independent.

Русский

Если семейство s_n возрастает и независимо, то iSup по направленному индексу и limsup вдоль фильтра независимы.

LaTeX

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

Lean4

theorem indep_biSup_limsup (h_le : ∀ n, s n ≤ m0) (h_indep : iIndep s κ μα) (hf : ∀ t, p t → tᶜ ∈ f) {t : Set ι}
    (ht : p t) : Indep (⨆ n ∈ t, s n) (limsup s f) κ μα :=
  by
  refine indep_of_indep_of_le_right (indep_biSup_compl h_le h_indep t) ?_
  refine limsSup_le_of_le (by isBoundedDefault) ?_
  simp only [Set.mem_compl_iff, eventually_map]
  exact eventually_of_mem (hf t ht) le_iSup₂

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