Subword complexity of the morphism a → aab, b → b

Let $a_n$ be the number of distinct subwords (contiguous factors) of length $n$ in the infinite word generated by the morphism $\sigma: a \mapsto aab, b \mapsto b$, starting from $a$.

The conjectured generating function is: $$\sum_{n \geq 0} a_n x^n = 1 + \frac{1}{1-x} + \frac{1}{(1-x)^2}\left(\frac{1}{1-x} - \sum_{k \geq 1} x^{2^k + k - 1}\right).$$

References:

• A6697
• J.-P. Allouche and J. Shallit, "On the subword complexity of the fixed point of a → aab, b → b, and generalizations," arXiv:1605.02361 [math.CO], 2016.
• N. J. A. Sloane and Simon Plouffe, The Encyclopedia of Integer Sequences, Academic Press, 1995.

def OeisA6697.morphism : Bool → List Bool

The morphism σ on {a, b} defined by a ↦ aab, b ↦ b, represented on Bool where false = a and true = b.

Equations

• OeisA6697.morphism false = [false, false, true]
• OeisA6697.morphism true = [true]

def OeisA6697.finiteWord : ℕ → List Bool

The n-th iterate of the morphism applied to [a].

Equations

• OeisA6697.finiteWord 0 = [false]
• OeisA6697.finiteWord n.succ = List.flatMap OeisA6697.morphism (OeisA6697.finiteWord n)

@[simp]

theorem OeisA6697.count_false_morphism (b : Bool) : List.count false (morphism b) = if b = true then 0 else 2

@[simp]

theorem OeisA6697.count_true_morphism (b : Bool) : List.count true (morphism b) = 1

@[simp]

theorem OeisA6697.count_false_finiteWord (n : ℕ) : List.count false (finiteWord n) = 2 ^ n

@[simp]

theorem OeisA6697.count_true_finiteWord (n : ℕ) : List.count true (finiteWord n) = 2 ^ n - 1

@[simp]

theorem OeisA6697.length_finiteWord (n : ℕ) : (finiteWord n).length = 2 ^ (n + 1) - 1

noncomputable def OeisA6697.infiniteWord (i : ℕ) : Bool

The infinite word w is the fixed point of the morphism starting from 'a'. We define it as the limit: w(i) is the i-th symbol, which stabilizes after sufficiently many iterations.

Equations

• OeisA6697.infiniteWord i = (OeisA6697.finiteWord (i + 1))[i]

noncomputable def OeisA6697.subwordAt (i n : ℕ) : List Bool

A subword (factor) of length n starting at position i.

Equations

• OeisA6697.subwordAt i n = List.map (fun (j : ℕ) => OeisA6697.infiniteWord (i + j)) (List.range n)

def OeisA6697.subwordsOfLength (n : ℕ) : Set (List Bool)

The set of all distinct subwords of length n in the infinite word.

Equations

• OeisA6697.subwordsOfLength n = {w : List Bool | ∃ (i : ℕ), w = OeisA6697.subwordAt i n}

noncomputable def OeisA6697.a (n : ℕ) : ℕ

The subword complexity function: a(n) is the number of distinct subwords of length n.

Equations

• OeisA6697.a n = (OeisA6697.subwordsOfLength n).ncard

theorem OeisA6697.conjecture (n : ℕ) : ↑(a n) = (PowerSeries.coeff n) (1 + (1 - PowerSeries.X)⁻¹ + (1 - PowerSeries.X)⁻¹ ^ 2 * ((1 - PowerSeries.X)⁻¹ - ∑' (k : ℕ), PowerSeries.X ^ (2 ^ (k + 1) + k)))

Conjecture (A6697): The generating function for the number of subwords of length $n$ in the infinite word generated by $a \mapsto aab, b \mapsto b$ is $$\sum_{n \geq 0} a_n x^n = 1 + \frac{1}{1-x} + \frac{1}{(1-x)^2}\left(\frac{1}{1-x} - \sum_{k \geq 0} x^{2^{k+1} + k}\right).$$

Equivalently, a(n) equals the n-th coefficient of this generating function.