English
Let u and v be bounded and nonnegative functions along a filter f; then limsup of their product is bounded above by the product of limsups: limsup (u v) ≤ (limsup u) (limsup v).
Русский
Пусть u и v регулярно ограничены и неотрицательны вдоль фильтра f; тогда limsup(u v) ≤ (limsup u)(limsup v).
LaTeX
$$$\limsup_{f} (u v) \le (\limsup_{f} u)(\limsup_{f} v).$$$
Lean4
theorem le_limsup_mul (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 f) * liminf v f ≤ limsup (u * 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₄
have u0 : 0 ≤ limsup u f := le_limsup_of_frequently_le h₁ h₂
have uv : 0 ≤ limsup (u * v) f :=
le_limsup_of_frequently_le ((h₁.and_eventually h₃).mono fun _ ⟨hu, hv⟩ ↦ mul_nonneg hu hv) h'
refine mul_le_of_forall_lt_of_nonneg u0 uv fun a a0 au b b0 bv ↦ ?_
refine (le_limsup_iff h h').2 fun c c_ab ↦ ?_
replace h₁ := IsCoboundedUnder.of_frequently_ge h₁
have h₅ := frequently_lt_of_lt_limsup h₁ au
have h₆ := eventually_lt_of_lt_liminf bv (isBoundedUnder_of_eventually_ge h₃)
apply (h₅.and_eventually (h₆.and h₃)).mono
exact fun x ⟨xa, ⟨xb, _⟩⟩ ↦ c_ab.trans_le <| mul_le_mul xa.le xb.le b0 (a0.trans xa.le)
