condIndep_limsup_atTop_self — Mathlib

English

Under standard conditions including StandardBorel Ω and IsFiniteMeasure μ, if iCondIndep holds for the family s, then the tail limsup along atTop is conditionally independent from itself: CondIndep m (limsup s atTop) (limsup s atTop) hm μ.

Русский

При стандартных условиях (StandardBorelΩ, IsFiniteMeasure μ) и условной независимости iCondIndep семейства s, хвостовая limsup вдоль atTop является условно независимой от самой себя: CondIndep m (limsup s atTop) (limsup s atTop) hm μ.

LaTeX

$$$\CondIndep\; m\; (\limsup s atTop)\; (\limsup s atTop)\; hm\ μ$$$

Lean4

theorem condIndep_limsup_atTop_self [StandardBorelSpace Ω] (hm : m ≤ m0) [IsFiniteMeasure μ] (h_le : ∀ n, s n ≤ m0)
    (h_indep : iCondIndep m hm s μ) : CondIndep m (limsup s atTop) (limsup s atTop) hm μ :=
  Kernel.indep_limsup_atTop_self h_le h_indep

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