English
If there is a nontrivial a such that a is in ns a for all n, independence between iSup s and limsup s f holds.
Русский
Если существует a, принадлежащий ns a для всех n, независимость между iSup s и limsup s f сохраняется.
LaTeX
$$$\\text{Indep}\\left(\\iSup_a \\iSup_n s_n, \\limsup s f\\right)\\mu$$$
Lean4
theorem indep_iSup_directed_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)) : Indep (⨆ a, ⨆ n ∈ ns a, s n) (limsup s f) κ μα :=
by
rcases eq_or_ne μα 0 with rfl | hμ
· simp
obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μα] η ∧ IsMarkovKernel η :=
exists_ae_eq_isMarkovKernel h_indep.ae_isProbabilityMeasure hμ
replace h_indep := h_indep.congr η_eq
apply Indep.congr (Filter.EventuallyEq.symm η_eq)
apply indep_iSup_of_directed_le
· exact fun a => indep_biSup_limsup h_le h_indep hf (hnsp a)
· exact fun a => iSup₂_le fun n _ => h_le n
· exact limsup_le_iSup.trans (iSup_le h_le)
· intro a b
obtain ⟨c, hc⟩ := hns a b
refine ⟨c, ?_, ?_⟩ <;> refine iSup_mono fun n => iSup_mono' fun hn => ⟨?_, le_rfl⟩
· exact hc.1 hn
· exact hc.2 hn
