English
Let f be a filter on a type α, and let u, v : α → EReal. If u takes nonnegative values frequently along f and v is nonnegative along f, then the product of limsup(u; f) and liminf(v; f) is bounded above by limsup of the product (u·v) along f.
Русский
Пусть f — фильтр на множество α, и пусть u, v : α → EReal. Если u принимает неотрицательные значения часто по f, а v неотрицателен по f, тогда произведение limsup(u; f) и liminf(v; f) не превосходит limsup(u·v; f).
LaTeX
$$$\\Bigl(\\exists^\\infty x\\in f,\\ 0 \\le u(x)\\Bigr) \\land \\Bigl(0 \\le^f v\\Bigr) \\Rightarrow \\limsup_f u \\cdot \\liminf_f v \\le \\limsup_f (u v)$$$
Lean4
theorem le_limsup_mul (hu : ∃ᶠ x in f, 0 ≤ u x) (hv : 0 ≤ᶠ[f] v) : limsup u f * liminf v f ≤ limsup (u * v) f :=
by
rcases f.eq_or_neBot with rfl | _
· rw [limsup_bot, limsup_bot, liminf_bot, bot_mul_top]
have u0 : 0 ≤ limsup u f := le_limsup_of_frequently_le hu
have uv0 : 0 ≤ limsup (u * v) f :=
le_limsup_of_frequently_le <| (hu.and_eventually hv).mono fun _ ⟨hu, hv⟩ ↦ mul_nonneg hu hv
refine mul_le_of_forall_lt_of_nonneg u0 uv0 fun a ha b hb ↦ (le_limsup_iff).2 fun c c_ab ↦ ?_
refine
(((frequently_lt_of_lt_limsup) (mem_Ioo.1 ha).2).and_eventually <|
(eventually_lt_of_lt_liminf (mem_Ioo.1 hb).2).and <| hv).mono
fun x ⟨xa, ⟨xb, vx⟩⟩ ↦ ?_
exact c_ab.trans_le (mul_le_mul xa.le xb.le (mem_Ioo.1 hb).1.le ((mem_Ioo.1 ha).1.le.trans xa.le))
