# 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.

## TODO #

Define a bundled `SubadditiveHom`

, use it.

The limit of a bounded-below subadditive sequence. The fact that the sequence indeed tends to
this limit is given in `Subadditive.tendsto_lim`

## Instances For

theorem
Subadditive.tendsto_lim
{u : ℕ → ℝ}
(h : Subadditive u)
(hbdd : BddBelow (Set.range fun (n : ℕ) => u n / ↑n))
:

Filter.Tendsto (fun (n : ℕ) => u n / ↑n) Filter.atTop (nhds h.lim)

Fekete's lemma: a subadditive sequence which is bounded below converges.