English
Under nonnegativity and boundedness hypotheses, limsup of the product is bounded above by the product of limsups: limsup (u v) ≤ (limsup u)(limsup v).
Русский
При условиях неотрицательности и ограниченности, limsup произведения не превосходит произведение limsup: limsup(u v) ≤ (limsup u)(limsup v).
LaTeX
$$$\limsup (u v) \le (\limsup u)(\limsup v).$$$
Lean4
theorem limsup_mul_le (h₁ : ∃ᶠ x in f, 0 ≤ u x) (h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u) (h₃ : 0 ≤ᶠ[f] v)
(h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v) : limsup (u * v) f ≤ (limsup u f) * limsup v f :=
by
have h :=
IsCoboundedUnder.of_frequently_ge (a := 0) <| (h₁.and_eventually h₃).mono fun x ⟨ux_0, vx_0⟩ ↦ mul_nonneg ux_0 vx_0
have h' := isBoundedUnder_le_mul_of_nonneg h₁ h₂ h₃ h₄
refine le_mul_of_forall_lt₀ fun a a_u b b_v ↦ (limsup_le_iff h h').2 fun c c_ab ↦ ?_
filter_upwards [eventually_lt_of_limsup_lt a_u, eventually_lt_of_limsup_lt b_v, h₃] with x x_a x_b v_0
apply lt_of_le_of_lt _ c_ab
rcases lt_or_ge (u x) 0 with u_0 | u_0
· apply (mul_nonpos_of_nonpos_of_nonneg u_0.le v_0).trans
exact mul_nonneg ((le_limsup_of_frequently_le h₁ h₂).trans a_u.le) (v_0.trans x_b.le)
· exact mul_le_mul x_a.le x_b.le v_0 (u_0.trans x_a.le)
