English
Let u,v : α → EReal with 0 ≤ᶠ[f] u and 0 ≤ᶠ[f] v. Then liminf u f · liminf v f ≤ liminf (u · v) f.
Русский
Пусть u, v : α → EReal и 0 ≤ᶠ[f] u, 0 ≤ᶠ[f] v. Тогда liminf u f · liminf v f ≤ liminf (u v) f.
LaTeX
$$$\\Bigl(0 \\le^f u\\Bigr) \\land \\Bigl(0 \\le^f v\\Bigr) \\\\Rightarrow \\\\ \\liminf_f u \\cdot \\liminf_f v \\\\le \\\\liminf_f (u v)$$
Lean4
theorem le_liminf_mul (hu : 0 ≤ᶠ[f] u) (hv : 0 ≤ᶠ[f] v) : liminf u f * liminf v f ≤ liminf (u * v) f :=
by
apply
mul_le_of_forall_lt_of_nonneg ((le_liminf_of_le) hu) <|
(le_liminf_of_le) ((hu.and hv).mono fun x ⟨u0, v0⟩ ↦ mul_nonneg u0 v0)
refine fun a ha b hb ↦ (le_liminf_iff).2 fun c c_ab ↦ ?_
filter_upwards [eventually_lt_of_lt_liminf (mem_Ioo.1 ha).2, eventually_lt_of_lt_liminf (mem_Ioo.1 hb).2] with x xa xb
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))
