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

def Subadditive (u : ) :

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

Instances For
def Subadditive.lim {u : } (_h : ) :

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 : ) (hbdd : BddBelow (Set.range fun n => u n / n)) {n : } (hn : n 0) :
u n / n
theorem Subadditive.apply_mul_add_le {u : } (h : ) (k : ) (n : ) (r : ) :
u (k * n + r) k * u n + u r
theorem Subadditive.eventually_div_lt_of_div_lt {u : } (h : ) {L : } {n : } (hn : n 0) (hL : u n / n < L) :
∀ᶠ (p : ) in Filter.atTop, u p / p < L
theorem Subadditive.tendsto_lim {u : } (h : ) (hbdd : BddBelow (Set.range fun n => u n / n)) :
Filter.Tendsto (fun n => u n / n) Filter.atTop ()

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