QuantumInfo.ForMathlib.Superadditive

Let $u: \mathbb{N} \to \mathbb{R}$ be a sequence of real numbers. The property `Superadditive` states that for all natural numbers $m$ and $n$, the sequence satisfies the inequality $u(m + n) \geq u(m) + u(n)$.

Let $u: \mathbb{N} \to \mathbb{R}$ be a sequence. If $u$ is a superadditive sequence, then the sequence defined by $n \mapsto -u(n)$ is a subadditive sequence.

Let $u: \mathbb{N} \to \mathbb{R}$ be a superadditive sequence (satisfying $u(m+n) \geq u(m) + u(n)$ for all $m, n \in \mathbb{N}$). The term $\text{lim}(u)$ is defined as the supremum of the set of values $\{\frac{u(n)}{n} : n \geq 1\}$.

Let $u: \mathbb{N} \to \mathbb{R}$ be a superadditive sequence. If the sequence $\{u(n)/n\}_{n \in \mathbb{N}}$ is bounded above, then $u(n)/n$ converges as $n \to \infty$ to its limit, denoted by $\text{lim}(u)$.

Let $u: \mathbb{N} \to \mathbb{R}$ be a sequence of real numbers. If $u$ is subadditive, then the sequence defined by $(-u)_n = -u_n$ is superadditive. That is, for all $m, n \in \mathbb{N}$, the inequality $-u_{m+n} \geq (-u_m) + (-u_n)$ holds.