Factor complexity of infinite words

DefinitionFactor of an infinite word#✓fully proved

A right-infinite word over an alphabet \(\alpha\) is a sequence \(u = u_0 u_1 u_2 \cdots\) of letters \(u_n \in \alpha\). For natural numbers \(k\) and \(i\), the length-\(k\) factor of \(u\) at position \(i\) is the word \(u_i u_{i+1} \cdots u_{i+k-1}\), given as the map \(\{0, \ldots, k-1\} \to \alpha\), \(s \mapsto u_{i+s}\).

def factor (u : ℕ → α) (k i : ℕ) : Fin k → α := fun s => u (i + s)
Used by 7
Used byThe all-zero word has no right-special factors · Factor as a list · Set of factors of a given length · Initial segment of an infinite word · Factors as lists and as tuples agree · Nonempty factors via list-valued factors · Factor complexity at length zero

DefinitionSet of factors of a given length#✓fully proved

For a right-infinite word \(u = u_0 u_1 u_2 \cdots\) over an alphabet \(\alpha\) and a natural number \(k\), the set of length-\(k\) factors of \(u\) is the set of the maps \(\{0, \ldots, k-1\} \to \alpha\), \(s \mapsto u_{i+s}\), for \(i \in \mathbb{N}\).

def factorSet (u : ℕ → α) (k : ℕ) : Set (Fin k → α) :=
  Set.range (factor u k)
Uses 1 · Used by 13
Statement usesFactor of an infinite word
Used byRight-special factors · The all-zero word has no right-special factors · Factors of the Thue–Morse word are closed under complement · Factor complexity of the Thue–Morse Quarto word versus Thue–Morse · Factor complexity of the Thue–Morse Quarto word at powers of two · Finitely many factors of each length · Factors as lists and as tuples agree · Factor complexity of an infinite word · Factor complexity at length zero · Maximum number of alternations in Thue–Morse factors · Minimum number of alternations in Thue–Morse factors · Reduced abelian complexity · Reduced factor complexity

DefinitionInitial segment of an infinite word#✓fully proved

For a right-infinite word \(u = u_0 u_1 u_2 \cdots\) over an alphabet \(\alpha\) and a natural number \(k\), the length-\(k\) initial segment of \(u\) is the word \(u_0 u_1 \cdots u_{k-1}\), given as the map \(\{0, \ldots, k-1\} \to \alpha\), \(s \mapsto u_s\); it is the length-\(k\) factor of \(u\) at position \(0\).

def initial (u : ℕ → α) (k : ℕ) : Fin k → α :=
  factor u k 0
Uses 1
Statement usesFactor of an infinite word

TheoremFinitely many factors of each length#✓fully proved

If the alphabet \(\alpha\) is finite, then for every right-infinite word \(u\) over \(\alpha\) and every natural number \(k\), the set of length-\(k\) factors of \(u\) is finite.

theorem finite_factorSet [Finite α] (u : ℕ → α) (k : ℕ) :
    (factorSet u k).Finite
Uses 1
Statement usesSet of factors of a given length

DefinitionFactor as a list#✓fully proved

For a right-infinite word \(u = u_0 u_1 u_2 \cdots\) over an alphabet \(\alpha\) and natural numbers \(k\) and \(i\), the length-\(k\) factor of \(u\) at position \(i\), as a list, is \([u_i, u_{i+1}, \ldots, u_{i+k-1}]\) (the empty list when \(k = 0\)).

def factorList (u : ℕ → α) (k i : ℕ) : List α :=
  List.ofFn (factor u k i)
Uses 1 · Used by 7
Statement usesFactor of an infinite word
Used byLists occurring in an infinite word · Occurrence via list-valued factors · Factors as lists and as tuples agree · Nonempty factors via list-valued factors · Nonempty factors are the factors that are nonempty · Words of frequency zero in almost every Mallows representation · Words without bounded gaps in almost every Mallows representation

DefinitionLists occurring in an infinite word#✓fully proved

A finite list \(w\) over an alphabet \(\alpha\) is a factor of a right-infinite word \(u = u_0 u_1 u_2 \cdots\) over \(\alpha\) when, writing \(\ell\) for the length of \(w\), there is a position \(i \in \mathbb{N}\) with \(w = [u_i, u_{i+1}, \ldots, u_{i+\ell-1}]\). In particular, the empty list is a factor of every right-infinite word over \(\alpha\).

def IsFactor (w : List α) (u : ℕ → α) : Prop :=
  ∃ i, factorList u w.length i = w
Uses 1 · Used by 6
Statement usesFactor as a list
Used byOccurrence via list-valued factors · Factors as lists and as tuples agree · Nonempty factors are the factors that are nonempty · Typical properties of Mallows representations · Transitive Mallows representations and continued fractions · Transitivity of the Mallows and Stern–Brocot representations

DefinitionNonempty factors of an infinite word#✓fully proved

Let \(u = u_0 u_1 u_2 \cdots\) be a right-infinite word over an alphabet \(\alpha\), viewed as a map \(\mathbb{N} \to \alpha\). A finite word \(w = w_0 w_1 \cdots w_{n-1}\) over \(\alpha\) is a nonempty factor of \(u\) when \(n \ge 1\) and there is a position \(i \in \mathbb{N}\) such that \(w_j = u_{i+j}\) for every \(j < n\).

The empty word is excluded, following the convention in which a factor is given by its endpoints \(r \le s\).

def IsNonemptyFactor (w : List α) (u : ℕ → α) : Prop :=
  w ≠ [] ∧ ∃ i, ∀ j (hj : j < w.length), w[j]'hj = u (i + j)
Used by 2
Used byNonempty factors via list-valued factors · Nonempty factors are the factors that are nonempty

TheoremOccurrence via list-valued factors#✓fully proved

Let \(w\) be a finite list of length \(\ell\) over an alphabet \(\alpha\) and \(u\) a right-infinite word over \(\alpha\). Then \(w\) is a factor of \(u\) if and only if there is a position \(i \in \mathbb{N}\) such that the length-\(\ell\) factor of \(u\) at position \(i\), as a list, equals \(w\).

theorem isFactor_iff_exists_factorList (w : List α) (u : ℕ → α) :
    IsFactor w u ↔ ∃ i, factorList u w.length i = w
Uses 2 · Used by 2
Statement usesLists occurring in an infinite word · Factor as a list
Used byFactors as lists and as tuples agree · Nonempty factors are the factors that are nonempty

TheoremNonempty factors via list-valued factors#✓fully proved

Let \(w\) be a finite list of length \(\ell\) over an alphabet \(\alpha\) and \(u = u_0 u_1 u_2 \cdots\) a right-infinite word over \(\alpha\). Then \(w\) is a nonempty factor of \(u\) if and only if \(w\) is nonempty and there is a position \(i \in \mathbb{N}\) with \([u_i, u_{i+1}, \ldots, u_{i+\ell-1}] = w\).

theorem isNonemptyFactor_iff_exists_factorList (w : List α) (u : ℕ → α) :
    IsNonemptyFactor w u ↔
      w ≠ [] ∧ ∃ i, factorList u w.length i = w
Uses 3 · Used by 1
Statement usesNonempty factors of an infinite word · Factor as a list
Proof usesFactor of an infinite word
Used byNonempty factors are the factors that are nonempty

TheoremNonempty factors are the factors that are nonempty#✓fully proved

For a finite list \(w\) over an alphabet \(\alpha\) and a right-infinite word \(u\) over \(\alpha\), \(w\) is a nonempty factor of \(u\) if and only if \(w\) is nonempty and \(w\) is a factor of \(u\).

theorem isNonemptyFactor_iff_isFactor_and_ne_nil (w : List α) (u : ℕ → α) :
    IsNonemptyFactor w u ↔ w ≠ [] ∧ IsFactor w u
Uses 5
Statement usesLists occurring in an infinite word · Nonempty factors of an infinite word
Proof usesFactor as a list · Occurrence via list-valued factors · Nonempty factors via list-valued factors

TheoremFactors as lists and as tuples agree#✓fully proved

Let \(k\) be a natural number, \(v\) a map \(\{0, \ldots, k-1\} \to \alpha\), written \(j \mapsto v_j\), and \(u\) a right-infinite word over \(\alpha\). Then the list \([v_0, v_1, \ldots, v_{k-1}]\) is a factor of \(u\) if and only if \(v\) belongs to the set of length-\(k\) factors of \(u\). This holds also for \(k = 0\).

theorem isFactor_ofFn_iff_mem_factorSet {k : ℕ} (v : Fin k → α) (u : ℕ → α) :
    IsFactor (List.ofFn v) u ↔ v ∈ factorSet u k
Uses 5
Statement usesLists occurring in an infinite word · Set of factors of a given length
Proof usesFactor of an infinite word · Factor as a list · Occurrence via list-valued factors

DefinitionFactor complexity of an infinite word#✓fully proved

Let \(w = w_0 w_1 w_2 \cdots\) be an infinite word over a finite alphabet \(A\). For \(n \ge 0\) and a position \(i \ge 0\), the factor of \(w\) of length \(n\) at position \(i\) is the word \(w_i w_{i+1} \cdots w_{i+n-1}\). The factor complexity \(p_w(n)\) is the number of distinct factors of \(w\) of length \(n\), each word being counted once however often it occurs in \(w\).

noncomputable def wordFactorComplexity {A : Type*} [Finite A]
    (w : ℕ → A) (n : ℕ) : ℕ :=
  Set.ncard (InfiniteWord.factorSet w n)
Sources
Uses 1 · Used by 11
Statement usesSet of factors of a given length
Used byFactor complexity of Kimberling's word · The meta-automatic sequences have linear factor complexity · Factor complexity of \(\mathcal{M}_2\) · Factor complexity of \(\mathcal{M}_2\) at powers of two · Factor complexity of the Thue–Morse Quarto word versus Thue–Morse · Factor complexity and right-special factors of the Thue–Morse Quarto word · Factor complexity of the Thue–Morse Quarto word at powers of two · First difference of the factor complexity of a binary word · Factor complexity at length zero · Pansiot's classification of the factor complexity of pure morphic words · Factor complexity of almost every Mallows representation

TheoremFactor complexity at length zero#✓fully proved

For every infinite word \(w\) over a finite alphabet, the factor complexity of \(w\) at length \(0\) equals \(1\), that is, \(p_w(0) = 1\): the empty word is the only factor of \(w\) of length \(0\).

theorem wordFactorComplexity_zero {A : Type*} [Finite A]
    (w : ℕ → A) : wordFactorComplexity w 0 = 1
Uses 3
Statement usesFactor complexity of an infinite word
Proof usesFactor of an infinite word · Set of factors of a given length
13 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.