Documentation

Mathlib.Analysis.Subadditive

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.

Equations
Instances For
    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
    Instances For
      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.