English
The limsup of a product is bounded above by the product of limsups: f.limsup (u · v) ≤ f.limsup u · f.limsup v.
Русский
Предел верхний произведения не превосходит произведение пределов верхних: limsup (u·v) ≤ limsup u · limsup v.
LaTeX
$$$\\\\forall f : \\text{Filter } α\\\\, [CountableInterFilter f] \\\\; (u v : α \\\\to \\\\mathbb{R}_{\\\\ge 0,\\\\infty}), \\\\; f.limsup (u \\cdot v) \\\\le f.limsup u \\\\cdot f.limsup v$$$
Lean4
/-- See also `limsup_mul_le'` -/
theorem limsup_mul_le [CountableInterFilter f] (u v : α → ℝ≥0∞) : f.limsup (u * v) ≤ f.limsup u * f.limsup v :=
calc
f.limsup (u * v) ≤ f.limsup fun x => f.limsup u * v x :=
by
refine limsup_le_limsup ?_
filter_upwards [@eventually_le_limsup _ f _ u] with x hx using mul_le_mul' hx le_rfl
_ = f.limsup u * f.limsup v := limsup_const_mul
