General theory of recurrences

C-finite, P-recursive and MC-finite sequences, Binet formulas, Skolem–Mahler–Lech, growth, generating functions and decomposable forms.

DefinitionP-recursive sequences#✓fully proved

Let \(r\) be a natural number, let \(P_0, \dots, P_r\) be polynomials with integer coefficients, and let \((u_n)_{n \ge 0}\) be a sequence of integers. The sequence \(u\) is P-recursive of order \(r\) with coefficient polynomials \(P_0, \dots, P_r\) if for every \(n \ge r\),

\[ P_0(n)\, u_n = \sum_{i=1}^{r} P_i(n)\, u_{n-i}. \]
public def IsPRecursiveSequence (r : ℕ) (P : Fin (r + 1) → Polynomial ℤ)
    (u : ℕ → ℤ) : Prop :=
  ∀ n, r ≤ n →
    (P 0).eval (n : ℤ) * u n =
      ∑ i : Fin r, (P i.succ).eval (n : ℤ) * u (n - (i + 1))
Used by 1
Used byP-recursive sequences with leading coefficient 1 are MC-finite

TheoremBinet formula for second-order linear recurrences#✓fully proved

Let \(K\) be a field, let \(P, Q, \alpha, \beta \in K\) with \(\alpha \ne \beta\), and suppose that \(\alpha\) and \(\beta\) are both roots of \(z^2 - Pz + Q\). If a sequence \(u : \mathbb{N} \to K\) satisfies \(u_{n+2} = P u_{n+1} - Q u_n\) for all \(n\), then for every natural number \(n\),

\[u_n = \frac{(u_1 - \beta u_0)\alpha^n - (u_1 - \alpha u_0)\beta^n}{\alpha - \beta}.\]
theorem binet_closed_form_second_order
    (u : ℕ → K) (P Q α β : K)
    (hα : α ^ 2 - P * α + Q = 0) (hβ : β ^ 2 - P * β + Q = 0)
    (hne : α ≠ β)
    (hrec : ∀ n : ℕ, u (n + 2) = P * u (n + 1) - Q * u n)
    (n : ℕ) :
    u n = ((u 1 - β * u 0) * α ^ n - (u 1 - α * u 0) * β ^ n) / (α - β)
Sources
Used by 2
Used byBinet formula for generalized Fibonacci sequences · Jacobsthal closed form

TheoremSkolem–Mahler–Lech theorem#✓fully proved

Let \(K\) be a field of characteristic zero, let \(k\) be a natural number, let \(c_0, \dots, c_{k-1} \in K\), and let \(u_0, u_1, u_2, \dots\) be a sequence in \(K\) satisfying the linear recurrence \(u_{n+k} = \sum_{i=0}^{k-1} c_i u_{n+i}\) for all \(n \ge 0\) (for \(k = 0\) the sum is empty and every \(u_n\) is \(0\)). Then there are a finite set \(F \subseteq \mathbb{N}\) and finitely many pairs \((a_1, d_1), \dots, (a_m, d_m)\) of natural numbers with every \(d_j > 0\) such that the zero set of the sequence is

\[\{n \in \mathbb{N} : u_n = 0\} = F \cup \bigcup_{j=1}^{m} \{a_j + d_j t : t \in \mathbb{N}\}.\]

The proof follows Lech's \(p\)-adic method: the data embed in \(\mathbb{Z}_p\) for a suitable prime \(p\) (a Cassels-type embedding), on each residue class modulo the period of the companion matrix modulo \(p\) the sequence is given by a convergent \(p\)-adic power series, and Strassmann's theorem bounds its zeros. C. Lech, A note on recurring series, Ark. Mat. 2 (1953), 417–421; J. W. S. Cassels, An embedding theorem for fields, Bull. Austral. Math. Soc. 14 (1976), 193–198.

public theorem skolemMahlerLech {K : Type*} [Field K] [CharZero K]
    (k : ℕ) (c : ℕ → K) (u : ℕ → K)
    (hrec : ∀ n, u (n + k) = ∑ i ∈ Finset.range k, c i * u (n + i)) :
    ∃ (F : Finset ℕ) (P : Finset (ℕ × ℕ)), (∀ p ∈ P, 0 < p.2) ∧
      {n | u n = 0} = ↑F ∪ ⋃ p ∈ (↑P : Set (ℕ × ℕ)), {n | ∃ t, n = p.1 + p.2 * t}
Sources
  • https://en.wikipedia.org/wiki/Skolem%E2%80%93Mahler%E2%80%93Lech_theorem (statement id skolem-lech-s1).
Uses 2
Proof usesStrassmann's theorem · Cassels' embedding theorem
3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.