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

A real-valued sequence is subadditive if it satisfies the inequality `u (m + n) ≤ u m + u n`

for all `m, n`

.

## Instances For

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.lim_le_div
{u : ℕ → ℝ}
(h : Subadditive u)
(hbdd : BddBelow (Set.range fun n => u n / ↑n))
{n : ℕ}
(hn : n ≠ 0)
:

Subadditive.lim h ≤ u n / ↑n

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 (Subadditive.lim h))

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