English
For β with countable index and appropriate filters f,g, the iterated limsup/liminf inequality holds: f.limsup (g.liminf (u a b)) ≤ g.liminf (f.limsup u a b).
Русский
Для β с счётной индексацией и подходящих фильтров выполняется неравенство: limsup_f (liminf_g (u)) ≤ liminf_g (limsup_f (u)).
LaTeX
$$$\\\\forall β [Countable β] [CountableInterFilter f] (g : \\text{Filter } β) (u : α \\to β \\to \\\\mathbb{R}_{\\\\ge 0,\\\\infty}), \\\\; f.limsup (\\\\lambda a. g.liminf (\\\\lambda b. u a b)) \\\\le g.liminf (\\\\lambda b. f.limsup (\\\\lambda a. u a b))$$$
Lean4
theorem limsup_liminf_le_liminf_limsup {β} [Countable β] {f : Filter α} [CountableInterFilter f] {g : Filter β}
(u : α → β → ℝ≥0∞) :
(f.limsup fun a : α => g.liminf fun b : β => u a b) ≤ g.liminf fun b => f.limsup fun a => u a b :=
have h1 : ∀ᶠ a in f, ∀ b, u a b ≤ f.limsup fun a' => u a' b :=
by
rw [eventually_countable_forall]
exact fun b => ENNReal.eventually_le_limsup fun a => u a b
sInf_le <| h1.mono fun x hx => Filter.liminf_le_liminf (Filter.Eventually.of_forall hx)
