limsup_mul_le' — Mathlib

English

A variant of the previous inequality with similar hypotheses, stating limsup(u·v) ≤ limsup(u)·limsup(v).

Русский

Вариант предыдущего неравенства с теми же гипотезами: limsup(u·v) ≤ limsup(u)·limsup(v).

LaTeX

$$$\limsup (u\cdot v) \leq \limsup u \cdot \limsup v$$$

Lean4

/-- See also `ENNReal.limsup_mul_le`. -/
theorem limsup_mul_le' (h : limsup u f ≠ 0 ∨ limsup v f ≠ ∞) (h' : limsup u f ≠ ∞ ∨ limsup v f ≠ 0) :
    limsup (u * v) f ≤ limsup u f * limsup v f :=
  by
  refine le_mul_of_forall_lt h h' fun a a_u b b_v ↦ (limsup_le_iff).2 fun c c_ab ↦ ?_
  filter_upwards [eventually_lt_of_limsup_lt a_u, eventually_lt_of_limsup_lt b_v] with x a_x b_x
  exact (mul_lt_mul a_x b_x).trans c_ab

Похожие утверждения