English
If h_le holds, and iIndep s κ μα holds, and directed relationships exist, then indep between iSup s and limsup s f holds with extra conditions about a.
Русский
Если выполняются условия h_le и iIndep s, существует направление, тогда независимость между iSup s и limsup s f сохраняется с дополнительными условиями относительно a.
LaTeX
$$$\\text{Indep}\\left(\\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) κ μα :=
by
suffices (⨆ a, ⨆ n ∈ ns a, s n) = ⨆ n, s n by
rw [← this]
exact indep_iSup_directed_limsup h_le h_indep hf hns hnsp
rw [iSup_comm]
refine iSup_congr fun n => ?_
have h : ⨆ (i : β) (_ : n ∈ ns i), s n = ⨆ _ : ∃ i, n ∈ ns i, s n := by rw [iSup_exists]
haveI : Nonempty (∃ i : β, n ∈ ns i) := ⟨hns_univ n⟩
rw [h, iSup_const]
