English
Let f be a filter on α, and u, v : α → EReal with u frequently nonnegative and v nonnegative along f. If limsup u(f) ≠ 0 or limsup v(f) ≠ ⊤, and if limsup u(f) ≠ ⊤ or limsup v(f) ≠ 0, then limsup of the product u·v along f is at most the product of limsup u(f) and limsup v(f).
Русский
Пусть f — фильтр на α и пусть u, v : α → EReal с условием, что u часто неотрицателен и v неотрицателен вдоль f. Если limsup u(f) не равен нулю или limsup v(f) не предел ⊤, и если limsup u(f) не равен ⊤ или limsup v(f) не равен нулю, тогда limsup(u·v) ≤ (limsup u)·(limsup v).
LaTeX
$$$\\Bigl(\\exists^\\infty x\\in f,\\ 0 \\le u(x)\\Bigr) \\land \\Bigl(0 \\le^f v\\Bigr) \\land \\bigl(\\limsup u f \\neq 0 \\lor \\limsup v f \\neq \\top\\bigr) \\land \\bigl(\\limsup u f \\neq \\top \\lor \\limsup v f \\neq 0\\bigr) \\\\Rightarrow \\\\ \\limsup_f (u v) \\\\le \\\\limsup_f u \\\\cdot \\\\limsup_f v$$
Lean4
theorem limsup_mul_le (hu : ∃ᶠ x in f, 0 ≤ u x) (hv : 0 ≤ᶠ[f] v) (h₁ : limsup u f ≠ 0 ∨ limsup v f ≠ ⊤)
(h₂ : limsup u f ≠ ⊤ ∨ limsup v f ≠ 0) : limsup (u * v) f ≤ limsup u f * limsup v f :=
by
rcases f.eq_or_neBot with rfl | _
· rw [limsup_bot]; exact bot_le
have u_0 : 0 ≤ limsup u f := le_limsup_of_frequently_le hu
replace h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤ := h₁.imp_left fun h ↦ lt_of_le_of_ne u_0 h.symm
replace h₂ : limsup u f ≠ ⊤ ∨ 0 < limsup v f :=
h₂.imp_right fun h ↦ lt_of_le_of_ne (le_limsup_of_frequently_le hv.frequently) h.symm
refine le_mul_of_forall_lt h₁ h₂ fun a a_u b b_v ↦ (limsup_le_iff).2 fun c c_ab ↦ ?_
filter_upwards [eventually_lt_of_limsup_lt a_u, eventually_lt_of_limsup_lt b_v, hv] with x x_a x_b v_0
apply lt_of_le_of_lt _ c_ab
rcases lt_or_ge (u x) 0 with hux | hux
· apply (mul_nonpos_iff.2 (.inr ⟨hux.le, v_0⟩)).trans
exact mul_nonneg (u_0.trans a_u.le) (v_0.trans x_b.le)
· exact mul_le_mul x_a.le x_b.le v_0 (hux.trans x_a.le)
