English
Under appropriate nondegeneracy conditions on u and v, linearGrowthInf (u+v) ≤ linearGrowthSup u + linearGrowthInf v.
Русский
При подходящих ненулевых предпосылках на u и v неверно, что линейный inf суммирования меньше или равен сумме верхнего роста u и нижнего роста v.
LaTeX
$$$\text{linearGrowthInf}(u+v) \le \text{linearGrowthSup}(u) + \text{linearGrowthInf}(v)\;\text{(under suitable nondegeneracy conditions)}$$$
Lean4
/-- See `linearGrowthInf_add_le'` for a version with swapped argument `u` and `v`. -/
theorem linearGrowthInf_add_le (h : linearGrowthSup u ≠ ⊥ ∨ linearGrowthInf v ≠ ⊤)
(h' : linearGrowthSup u ≠ ⊤ ∨ linearGrowthInf v ≠ ⊥) :
linearGrowthInf (u + v) ≤ linearGrowthSup u + linearGrowthInf v :=
by
refine (liminf_add_le h h').trans_eq' (liminf_congr (Eventually.of_forall fun n ↦ ?_))
rw [Pi.add_apply, Pi.add_apply, ← add_div_of_nonneg_right n.cast_nonneg']
