# Convergence of subadditive sequences #

A subadditive sequence u : ℕ → ℝ is a sequence satisfying u (m + n) ≤ u m + u n for all m, n. We define this notion as subadditive u, and prove in subadditive.tendsto_lim that, if u n / n is bounded below, then it converges to a limit (that we denote by subadditive.lim for convenience). This result is known as Fekete's lemma in the literature.

def subadditive (u : ) :
Prop

A real-valued sequence is subadditive if it satisfies the inequality u (m + n) ≤ u m + u n for all m, n.

Equations
@[protected, nolint, irreducible]
The limit of a bounded-below subadditive sequence. The fact that the sequence indeed tends to this limit is given in subadditive.tendsto_lim