Regular sequences

Definition\(k\)-regular sequence#✓fully proved

Let \(k\) be a natural number. An integer sequence \(f : \mathbb{N} \to \mathbb{Z}\) is \(k\)-regular, in the sense of Allouche and Shallit, if \(k \ge 2\) and the \(\mathbb{Z}\)-submodule of the module of all integer sequences spanned by the \(k\)-kernel of \(f\) is finitely generated.

def IsKRegularSequence (k : ℕ) (f : ℕ → ℤ) : Prop :=
  2 ≤ k ∧ (Submodule.span ℤ (kKernel k f)).FG

Sources

• John M. Campbell and Benoît Cloitre, Meta-Automatic Sequences, Journal of Integer Sequences 29 (2026), Article 26.4.1, Lemma 28 (k-regular sequences of Allouche and Shallit) and Definition 1 (k-kernel).

Uses 1 · Used by 3

Statement usesThe \(k\)-kernel of a sequence

Used byRight-special factor counts of automatic sequences are regular · Constant sequences are \(k\)-regular · The base of a \(k\)-regular sequence is at least 2

TheoremConstant sequences are \(k\)-regular#✓fully proved

For every natural number \(k \ge 2\) and every integer \(c\), the constant sequence \(n \mapsto c\) is \(k\)-regular.

theorem isKRegularSequence_const {k : ℕ} (hk : 2 ≤ k) (c : ℤ) :
    IsKRegularSequence k (fun _ => c)

Sources

• John M. Campbell and Benoît Cloitre, Meta-Automatic Sequences, Journal of Integer Sequences 29 (2026), Article 26.4.1, Lemma 28.

Uses 2

Statement uses\(k\)-regular sequence

Proof usesThe \(k\)-kernel of a sequence

TheoremThe base of a \(k\)-regular sequence is at least 2#✓fully proved

Let \(k\) be a natural number. If an integer sequence \(f\) is \(k\)-regular, then \(k \ge 2\).

theorem IsKRegularSequence.two_le {k : ℕ} {f : ℕ → ℤ} (h : IsKRegularSequence k f) : 2 ≤ k

Sources

• John M. Campbell and Benoît Cloitre, Meta-Automatic Sequences, Journal of Integer Sequences 29 (2026), Article 26.4.1, Lemma 28.

Uses 2

Statement uses\(k\)-regular sequence

Proof usesThe \(k\)-kernel of a sequence

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.