C-finite sequences

DefinitionC-finite integer sequences#✓fully proved

An integer sequence \(s \colon \mathbb{N} \to \mathbb{Z}\) is C-finite if there are \(p, q \in \mathbb{N}\) and integers \(c_0, \dots, c_{p-1}\) such that \(s(n + p) = \sum_{i=0}^{p-1} c_i \, s(n + i)\) for every \(n \ge q\).

def IsIntegerCFiniteSequence (s : ℕ → ℤ) : Prop :=
  ∃ p q, ∃ c : Fin p → ℤ, ∀ n, q ≤ n → s (n + p) = ∑ i, c i * s (n + (i : ℕ))

Sources

• JIS VOL26/Fischer–Kotek–Makowsky, https://cs.uwaterloo.ca/journals/JIS/VOL26/Makowsky/makowsky16.tex, lines 249–259.

Used by 2

Used byA tail of a C-finite sequence satisfies a linear recurrence · Solutions of linear recurrences are C-finite

TheoremSolutions of linear recurrences are C-finite#✓fully proved

Let \(p \in \mathbb{N}\) and let \(c_0, \dots, c_{p-1}\) be integers. If an integer sequence \(s\) satisfies \(s(n + p) = \sum_{i=0}^{p-1} c_i \, s(n + i)\) for every \(n \in \mathbb{N}\), then \(s\) is C-finite.

theorem isIntegerCFiniteSequence_of_isSolution (E : LinearRecurrence ℤ) (s : ℕ → ℤ)
    (h : E.IsSolution s) : IsIntegerCFiniteSequence s

Uses 1

Statement usesC-finite integer sequences

TheoremDiscarding the exceptional prefix of a C-finite recurrence#✓fully proved

Let \(s\) be an integer sequence, let \(p, q \in \mathbb{N}\) and let \(c_0, \dots, c_{p-1}\) be integers. If \(s(n + p) = \sum_{i=0}^{p-1} c_i \, s(n + i)\) for every \(n \ge q\), then the shifted sequence \(t(n) = s(n + q)\) satisfies \(t(n + p) = \sum_{i=0}^{p-1} c_i \, t(n + i)\) for every \(n \in \mathbb{N}\).

theorem isSolution_tail_of_cFiniteWitness (s : ℕ → ℤ) (p q : ℕ) (c : Fin p → ℤ)
    (h : ∀ n, q ≤ n → s (n + p) = ∑ i, c i * s (n + (i : ℕ))) :
    (LinearRecurrence.mk p c).IsSolution (fun n => s (n + q))

Used by 1

Used byA tail of a C-finite sequence satisfies a linear recurrence

TheoremA tail of a C-finite sequence satisfies a linear recurrence#✓fully proved

If an integer sequence \(s\) is C-finite, then there are a shift \(q \in \mathbb{N}\), an order \(p \in \mathbb{N}\) and integers \(c_0, \dots, c_{p-1}\) such that the shifted sequence \(t(n) = s(n + q)\) satisfies \(t(n + p) = \sum_{i=0}^{p-1} c_i \, t(n + i)\) for every \(n \in \mathbb{N}\).

theorem IsIntegerCFiniteSequence.exists_isSolution_tail {s : ℕ → ℤ}
    (h : IsIntegerCFiniteSequence s) :
    ∃ (E : LinearRecurrence ℤ) (q : ℕ), E.IsSolution (fun n => s (n + q))

Uses 2

Statement usesC-finite integer sequences

Proof usesDiscarding the exceptional prefix of a C-finite recurrence

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.