le_linearGrowthSup_add — Mathlib

English

For sequences u,v with suitable nondegeneracy, linearGrowthInf (u+v) ≤ linearGrowthSup u + linearGrowthInf v.

Русский

Для последовательностей с подходящими невыраженными условиями, линейный inf рост от суммы не превышает верхний рост u плюс нижний рост v.

LaTeX

$$$\operatorname{linearGrowthInf}(u+v) \le \operatorname{linearGrowthSup}(u) + \operatorname{linearGrowthInf}(v)$$$

Lean4

/-- See `le_linearGrowthSup_add'` for a version with swapped argument `u` and `v`. -/
theorem le_linearGrowthSup_add : linearGrowthSup u + linearGrowthInf v ≤ linearGrowthSup (u + v) :=
  by
  refine le_limsup_add.trans_eq (limsup_congr (Eventually.of_forall fun n ↦ ?_))
  rw [Pi.add_apply, Pi.add_apply, add_div_of_nonneg_right n.cast_nonneg']

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