mathlib3 documentation

analysis.subadditive

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.

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
@[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
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
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) :
theorem subadditive.tendsto_lim {u : } (h : subadditive u) (hbdd : bdd_below (set.range (λ (n : ), u n / n))) :

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