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 Submultiplicative {α : Type u_1} {β : Type u_2} [Add α] [Mul β] [LE β] (u : α → β) : Prop

A sequence is submultiplicative if it satisfies the inequality u (m + n) ≤ u m * u n for all m, n.

Equations

• Submultiplicative u = ∀ (m n : α), u (m + n) ≤ u m * u n

def Subadditive {α : Type u_1} {β : Type u_2} [Add α] [Add β] [LE β] (u : α → β) : Prop

A 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

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

The limit of the nth roots of a submultiplicative sequence. The fact that the nth roots indeed converge to this limit is given in Submultiplicative.tendsto_lim.

Equations

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

theorem Submultiplicative.lim_le_rpow {u : ℕ → ℝ} (h : Submultiplicative u) (hbdd : ∀ (n : ℕ), 0 ≤ u n) {n : ℕ} (hn : n ≠ 0) : h.lim ≤ u n ^ (↑n)⁻¹

theorem Submultiplicative.apply_mul_add_le {u : ℕ → ℝ} (h : Submultiplicative u) (k n r : ℕ) (hbdd : 0 ≤ u n) : u (k * n + r) ≤ u n ^ k * u r

theorem Submultiplicative.eventually_rpow_lt_of_rpow_lt {u : ℕ → ℝ} (h : Submultiplicative u) (hbdd : ∀ (k : ℕ), 0 ≤ u k) {L : ℝ} {n : ℕ} (hn : n ≠ 0) (hL : u n ^ (↑n)⁻¹ < L) : ∀ᶠ (p : ℕ) in Filter.atTop, u p ^ (↑p)⁻¹ < L

theorem Submultiplicative.tendsto_lim {u : ℕ → ℝ} (h : Submultiplicative u) (hbdd : ∀ (n : ℕ), 0 ≤ u n) : Filter.Tendsto (fun (n : ℕ) => u n ^ (↑n)⁻¹) Filter.atTop (nhds h.lim)

Fekete's lemma for nonnegative submultiplicative sequences: The nth roots of a submultiplicative sequence converge.

@[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 = 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

@[deprecated "This was used solely to prove `Subadditive.tendsto_lim` which is now proved directly from the multiplicative version." (since := "2026-08-20")]

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.submultiplicative_exp {u : ℕ → ℝ} (h : Subadditive u) : Submultiplicative fun (n : ℕ) => Real.exp (u 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 h.lim)

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