English
Under nonnegativity and boundedness hypotheses, liminf of the product is bounded above by the product of liminfs/limsups: liminf (u v) ≤ (limsup u) (liminf v).
Русский
При неотрицательности и ограниченности, liminf произведения ≤ (limsup u) (liminf v).
LaTeX
$$$\liminf (u v) \le (\limsup u)(\liminf v).$$$
Lean4
theorem liminf_mul_le [f.NeBot] (h₁ : 0 ≤ᶠ[f] u) (h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u) (h₃ : 0 ≤ᶠ[f] v)
(h₄ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f v) : liminf (u * v) f ≤ (limsup u f) * liminf v f :=
by
have h := isCoboundedUnder_ge_mul_of_nonneg h₁ h₂ h₃ h₄
have h' := isBoundedUnder_of_eventually_ge (a := 0) <| (h₁.and h₃).mono fun x ⟨u_0, v_0⟩ ↦ mul_nonneg u_0 v_0
refine le_mul_of_forall_lt₀ fun a a_u b b_v ↦ (liminf_le_iff h h').2 fun c c_ab ↦ ?_
refine
((frequently_lt_of_liminf_lt h₄ b_v).and_eventually ((eventually_lt_of_limsup_lt a_u).and (h₁.and h₃))).mono
fun x ⟨x_v, x_u, u_0, v_0⟩ ↦ ?_
exact (mul_le_mul x_u.le x_v.le v_0 (u_0.trans x_u.le)).trans_lt c_ab
