English
Let s be a family of sub-sigma-algebras dominated by m0, and let κ or μ provide independence iIndep. Then the limsup along atTop, limsup s atTop, is independent of itself: Indep(limsup s atTop, limsup s atTop).
Русский
Пусть имеется семейство подп_sigma-алгебр, ограниченное m0, и независимо относительно μ (или κ). Тогда хвостовая лимсап вдоль atTop независима сама от себя: Indep(limsup s atTop, limsup s atTop).
LaTeX
$$$\Indep(\limsup s\, atTop, \limsup s\, atTop)\, μ$$$
Lean4
theorem indep_limsup_atTop_self (h_le : ∀ n, s n ≤ m0) (h_indep : iIndep s κ μα) :
Indep (limsup s atTop) (limsup s atTop) κ μα :=
by
let ns : ι → Set ι := Set.Iic
have hnsp : ∀ i, BddAbove (ns i) := fun i => bddAbove_Iic
refine indep_limsup_self h_le h_indep ?_ ?_ hnsp ?_
· simp only [mem_atTop_sets, Set.mem_compl_iff, BddAbove, upperBounds, Set.Nonempty]
rintro t ⟨a, ha⟩
obtain ⟨b, hb⟩ : ∃ b, a < b := exists_gt a
refine ⟨b, fun c hc hct => ?_⟩
suffices ∀ i ∈ t, i < c from lt_irrefl c (this c hct)
exact fun i hi => (ha hi).trans_lt (hb.trans_le hc)
· exact Monotone.directed_le fun i j hij k hki => le_trans hki hij
· exact fun n => ⟨n, le_rfl⟩
