The k-kernel of a sequence and Eilenberg's theorem

The k-kernel of a sequence a : ℕ → Δ is the set of its subsequences n ↦ a (k ^ e * n + r) with r < k ^ e. Eilenberg's theorem characterises the k-automatic sequences, for 2 ≤ k, as those with a finite k-kernel. This is the form in which automaticity is established in the proof of Christol's theorem, where the kernel of the coefficient sequence of an algebraic power series is the orbit of the series under the Cartier operators, and in the comparison of automaticity in the bases k and k ^ m.

The kernel is closed under the transitions b ↦ (n ↦ b (k * n + d)) with d < k, so it is the state set of an automaton with output b ↦ b 0, the kernel automaton TauCeti.kernelDFAO. Reading the digits of n least significant digit first from the state a, it outputs a n; it does so on every base-k representation of n, including those padded with trailing zeros.

Main definitions and results

• TauCeti.kernel k a: the k-kernel of a.
• TauCeti.self_mem_kernel, TauCeti.kernel_subset: a sequence lies in its kernel, and the kernel of a kernel element is contained in the kernel.
• TauCeti.kernel_subset_of_mem_of_forall: the kernel of a is contained in every set that contains a and is closed under the transitions b ↦ (n ↦ b (k * n + d)) with d < k.
• TauCeti.kernelDFAO k a: the kernel automaton, and TauCeti.output_eval_kernelDFAO: on any word of digits it outputs a at the value of the word.
• TauCeti.isAutomatic_iff_finite_kernel: Eilenberg's theorem, for 2 ≤ k a sequence is k-automatic if and only if its k-kernel is finite.

References

• Jakub Byszewski, Jakub Konieczny, Automatic sequences and generalised polynomials, Canad. J. Math. 72 (2020), Section 1, Definition 1.4.
• Andrew Bridy, Automatic sequences and curves over finite fields, Algebra & Number Theory 11 (2017), Section 2.1, Theorem 2.2.
• Eric Rowland, Manon Stipulanti, Reem Yassawi, An elementary proof of Bridy's theorem, Section 3.

def TauCeti.kernel {Δ : Type u} (k : ℕ) (a : ℕ → Δ) : Set (ℕ → Δ)

The k-kernel of a sequence a: the set of its subsequences n ↦ a (k ^ e * n + r) with e : ℕ and r < k ^ e.

theorem TauCeti.mem_kernel {k : ℕ} {Δ : Type u} {a b : ℕ → Δ} : b ∈ kernel k a ↔ ∃ (e : ℕ), ∃ r < k ^ e, b = fun (n : ℕ) => a (k ^ e * n + r)

Membership in the k-kernel, unfolded.

@[simp]

theorem TauCeti.self_mem_kernel {Δ : Type u} (k : ℕ) (a : ℕ → Δ) : a ∈ kernel k a

A sequence belongs to its own kernel, with e = 0 and r = 0.

theorem TauCeti.apply_mul_add_mem_kernel {k : ℕ} {Δ : Type u} {a : ℕ → Δ} {d : ℕ} (hd : d < k) : (fun (n : ℕ) => a (k * n + d)) ∈ kernel k a

The subsequence n ↦ a (k * n + d) with d < k belongs to the k-kernel of a.

theorem TauCeti.kernel_subset {k : ℕ} {Δ : Type u} {a b : ℕ → Δ} (hb : b ∈ kernel k a) : kernel k b ⊆ kernel k a

The kernel of an element of the kernel of a is contained in the kernel of a.

theorem TauCeti.kernel_subset_of_mem_of_forall {k : ℕ} {Δ : Type u} {a : ℕ → Δ} {S : Set (ℕ → Δ)} (ha : a ∈ S) (hS : ∀ b ∈ S, ∀ d < k, (fun (n : ℕ) => b (k * n + d)) ∈ S) : kernel k a ⊆ S

The k-kernel of a is contained in every set of sequences that contains a and is closed under the transitions b ↦ (n ↦ b (k * n + d)) with d < k.

@[simp]

theorem TauCeti.kernel_const {Δ : Type u} (k : ℕ) (x : Δ) : (kernel k fun (x_1 : ℕ) => x) = {fun (x_1 : ℕ) => x}

The kernel of a constant sequence is the singleton of that sequence.

The kernel automaton

def TauCeti.kernelDFAO {Δ : Type u} (k : ℕ) (a : ℕ → Δ) : DFAO (Fin k) (↑(kernel k a)) Δ

The kernel automaton of a: its states are the elements of the k-kernel of a, its initial state is a, its output is the value at 0, and on the digit d it moves from b to n ↦ b (k * n + d).

@[simp]

theorem TauCeti.coe_kernelDFAO_step {k : ℕ} {Δ : Type u} {a : ℕ → Δ} (b : ↑(kernel k a)) (d : Fin k) : ↑((kernelDFAO k a).step b d) = fun (n : ℕ) => ↑b (k * n + ↑d)

@[simp]

theorem TauCeti.coe_kernelDFAO_start {k : ℕ} {Δ : Type u} {a : ℕ → Δ} : ↑(kernelDFAO k a).start = a

@[simp]

theorem TauCeti.kernelDFAO_output {k : ℕ} {Δ : Type u} {a : ℕ → Δ} (b : ↑(kernel k a)) : (kernelDFAO k a).output b = ↑b 0

@[simp]

theorem TauCeti.coe_kernelDFAO_evalFrom {k : ℕ} {Δ : Type u} {a : ℕ → Δ} (b : ↑(kernel k a)) (w : List (Fin k)) : ↑((kernelDFAO k a).evalFrom b w) = fun (n : ℕ) => ↑b (k ^ w.length * n + Nat.ofDigits k (List.map Fin.val w))

From the state b, after reading the word w the kernel automaton is in the state n ↦ b (k ^ |w| * n + v), where v is the value of w read least significant digit first.

@[simp]

theorem TauCeti.coe_kernelDFAO_eval {k : ℕ} {Δ : Type u} {a : ℕ → Δ} (w : List (Fin k)) : ↑((kernelDFAO k a).eval w) = fun (n : ℕ) => a (k ^ w.length * n + Nat.ofDigits k (List.map Fin.val w))

After reading the word w the kernel automaton of a is in the state n ↦ a (k ^ |w| * n + v), where v is the value of w read least significant digit first.

theorem TauCeti.output_eval_kernelDFAO {k : ℕ} {Δ : Type u} {a : ℕ → Δ} (w : List (Fin k)) : (kernelDFAO k a).output ((kernelDFAO k a).eval w) = a (Nat.ofDigits k (List.map Fin.val w))

The kernel automaton of a outputs a at the value of any word of base-k digits, read least significant digit first. Trailing zeros are allowed: the output only depends on the value of the word.

Eilenberg's theorem

theorem TauCeti.IsAutomatic.finite_kernel {k : ℕ} {Δ : Type u} {a : ℕ → Δ} [NeZero k] (ha : IsAutomatic k a) : (kernel k a).Finite

A k-automatic sequence has a finite k-kernel.

theorem TauCeti.isAutomatic_of_finite_kernel {k : ℕ} {Δ : Type u} {a : ℕ → Δ} [NeZero k] (hk : 2 ≤ k) (h : (kernel k a).Finite) : IsAutomatic k a

For 2 ≤ k, a sequence with a finite k-kernel is k-automatic: the kernel automaton computes it.

theorem TauCeti.isAutomatic_iff_finite_kernel {k : ℕ} {Δ : Type u} {a : ℕ → Δ} [NeZero k] (hk : 2 ≤ k) : IsAutomatic k a ↔ (kernel k a).Finite

Eilenberg's theorem: for 2 ≤ k, a sequence is k-automatic if and only if its k-kernel is finite.

Checks