Subadditive.tendsto_lim

theorem Subadditive.tendsto_lim : ∀ {u : ℕ → ℝ} (h : Subadditive u), BddBelow (Set.range fun n => u n / ↑n) → Filter.Tendsto (fun n => u n / ↑n) Filter.atTop (nhds h.lim)

Fekete's lemma states that if we have a sequence of real numbers `u` that is subadditive (meaning for all natural numbers `m`, `n`, `u (m + n)` is less than or equal to `u m + u n`), and the set of ratios of `u n` to `n` is bounded below, then the sequence of these ratios tends to a limit as `n` approaches infinity. The limit is defined as a value `x` such that for every neighborhood of `x`, the preimage of `x` under the function defining the sequence is a neighborhood of `n` in the filter representing the limit `→ ∞`.

More concisely: If a subadditive sequence of real numbers `u` has a bounded below ratio sequence, then `u` converges to its liminf as `n` approaches infinity.