limsup_add_le — Mathlib

English

A general inequality bounding limsup of sums by the sum of limsups, under mild non-extremal conditions.

Русский

Обобщённое неравенство, ограничивающее лимсуп суммы суммой лимсупов при слабых неоднородностях.

LaTeX

$$$ \limsup (u+v) \le \limsup u + \limsup v $ under mild conditions $$$

Lean4

theorem limsup_add_le (h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤) (h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥) :
    limsup (u + v) f ≤ (limsup u f) + (limsup v f) :=
  by
  refine le_add_of_forall_gt 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 (add_lt_add a_x b_x).trans c_ab

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