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 : ℕ → ℝ) : Prop

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

Equations

• Subadditive u = ∀ (m n : ℕ), u (m + n) ≤ u m + u n

def Subadditive.lim {u : ℕ → ℝ} (_h : Subadditive u) : ℝ

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

Equations

• _h.lim = sInf ((fun (n : ℕ) => u n / ↑n) '' Set.Ici 1)

theorem Subadditive.lim_le_div {u : ℕ → ℝ} (h : Subadditive u) (hbdd : BddBelow (Set.range fun (n : ℕ) => u n / ↑n)) {n : ℕ} (hn : n ≠ 0) : h.lim ≤ u n / ↑n

theorem Subadditive.apply_mul_add_le {u : ℕ → ℝ} (h : Subadditive u) (k n r : ℕ) : u (k * n + r) ≤ ↑k * u n + u r

theorem Subadditive.eventually_div_lt_of_div_lt {u : ℕ → ℝ} (h : Subadditive u) {L : ℝ} {n : ℕ} (hn : n ≠ 0) (hL : u n / ↑n < L) : ∀ᶠ (p : ℕ) in Filter.atTop, u p / ↑p < L

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.