Convergence of subadditive sequences #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source

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

source

@[protected, nolint, irreducible]

noncomputable 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 = has_Inf.Inf ((λ (n : ℕ), u n / ↑n) '' set.Ici 1)

source

theorem subadditive.lim_le_div {u : ℕ → ℝ} (h : subadditive u) (hbdd : bdd_below (set.range (λ (n : ℕ), u n / ↑n))) {n : ℕ} (hn : n ≠ 0) :

h.lim ≤ u n / ↑n

source

theorem subadditive.apply_mul_add_le {u : ℕ → ℝ} (h : subadditive u) (k n r : ℕ) :

u (k * n + r) ≤ ↑k * u n + u r

source

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.at_top , u p / ↑p < L

source

theorem subadditive.tendsto_lim {u : ℕ → ℝ} (h : subadditive u) (hbdd : bdd_below (set.range (λ (n : ℕ), u n / ↑n))) :

filter.tendsto (λ (n : ℕ), u n / ↑n) filter.at_top (nhds h.lim)

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