Growth of linear recurrence sequences

TheoremExponential growth bound for solutions of linear recurrences#✓fully proved

Let \(k\) be a natural number, let \(c_0, \dots, c_{k-1}\) be complex numbers, and let \(t : \mathbb{N} \to \mathbb{C}\) satisfy \(t(n+k) = \sum_{i=0}^{k-1} c_i \, t(n+i)\) for all \(n \in \mathbb{N}\). Then there is an integer \(g \ge 1\) such that \(|t(n)| < g^{n+1}\) for all \(n \in \mathbb{N}\).

theorem exists_norm_lt_pow_of_isSolution (E : LinearRecurrence ℂ) (t : ℕ → ℂ)
    (h : E.IsSolution t) :
    ∃ g : ℤ, 1 ≤ g ∧ ∀ n : ℕ, ‖t n‖ < ((g : ℝ) ^ (n + 1))

Used by 1

Used byExponential growth bound for C-recursive sequences

TheoremExponential growth bound for C-recursive sequences#✓fully proved

Let \(t : \mathbb{N} \to \mathbb{C}\) be C-recursive: there are an order \(k \ge 1\) and complex numbers \(c_0, \dots, c_{k-1}\) with \(t(n+k) = \sum_{i=0}^{k-1} c_i \, t(n+i)\) for all \(n \in \mathbb{N}\). Then there is an integer \(g \ge 1\) such that \(|t(n)| < g^{n+1}\) for all \(n \in \mathbb{N}\).

theorem c_recursive_exponential_growth_bound
    (t : ℕ → ℂ)
    (h : ∃ k : ℕ, 1 ≤ k ∧ ∃ c : Fin k → ℂ,
      ∀ n : ℕ, t (n + k) = ∑ i : Fin k, c i * t (n + i.val)) :
    ∃ g : ℤ, 1 ≤ g ∧ ∀ n : ℕ, ‖t n‖ < ((g : ℝ) ^ (n + 1))

Sources

• M. Prunescu and J. M. Shunia, "On Modular Representations of C-Recursive Integer Sequences," Journal of Integer Sequences 28 (2025), Article 25.5.3, Lemma (quoting Prunescu and Sauras-Altuzarra, Lemma 4), lines 166–167, https://cs.uwaterloo.ca/journals/JIS/VOL28/Prunescu/prunescu3.tex

Uses 1

Proof usesExponential growth bound for solutions of linear recurrences

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.