English
Let s be a family of sub-sigma-algebras dominated by m0 with μ finite; then the tail limsup atBot is independent from itself: Indep(limsup s atBot) (limsup s atBot) μ.
Русский
Пусть s — семейство подп_sigma-алгебр, ограниченное m0, μ конечна; хвостовая limsup в atBot независима сама от себя.
LaTeX
$$$\Indep(\limsup s atBot, \limsup s atBot)\; μ$$$
Lean4
theorem indep_limsup_atBot_self (h_le : ∀ n, s n ≤ m0) (h_indep : iIndep s κ μα) :
Indep (limsup s atBot) (limsup s atBot) κ μα :=
by
let ns : ι → Set ι := Set.Ici
have hnsp : ∀ i, BddBelow (ns i) := fun i => bddBelow_Ici
refine indep_limsup_self h_le h_indep ?_ ?_ hnsp ?_
· simp only [mem_atBot_sets, Set.mem_compl_iff, BddBelow, lowerBounds, Set.Nonempty]
rintro t ⟨a, ha⟩
obtain ⟨b, hb⟩ : ∃ b, b < a := exists_lt a
refine ⟨b, fun c hc hct => ?_⟩
suffices ∀ i ∈ t, c < i from lt_irrefl c (this c hct)
exact fun i hi => hc.trans_lt (hb.trans_le (ha hi))
· exact Antitone.directed_le fun _ _ ↦ Set.Ici_subset_Ici.2
· exact fun n => ⟨n, le_rfl⟩
