le_linearGrowthInf_add — Mathlib

English

For sequences u,v: ℕ→EReal the infimum of the sum is bounded above by the sum of infima: linearGrowthInf (u+v) ≤ linearGrowthInf u + linearGrowthInf v.

Русский

Для последовательностей u, v: ℕ → EReal справедливо неравенство: линейный inf-рост от суммы не превосходит суммы линейных inf-ростов.

LaTeX

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

Lean4

theorem le_linearGrowthInf_add : linearGrowthInf u + linearGrowthInf v ≤ linearGrowthInf (u + v) :=
  by
  refine le_liminf_add.trans_eq (liminf_congr (Eventually.of_forall fun n ↦ ?_))
  rw [Pi.add_apply, Pi.add_apply, ← add_div_of_nonneg_right n.cast_nonneg']

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