Lyndon and primitive words

DefinitionPrimitive word#✓fully proved

A nonempty finite word is primitive if it is not a proper power of another word.

def IsPrimitiveWord {α : Type*} (u : List α) : Prop :=
  u ≠ [] ∧ ∀ (v : List α) (n : ℕ), List.flatten (List.replicate n v) = u → n = 1

Used by 5

Used byWitt's formula for the number of Lyndon words of given content · Primitivity via distinct rotations · Lyndon words are primitive · Primitive words of given content · Nontrivial rotations move a primitive word

DefinitionContent of a word#✓fully proved

Let \(r\) be a natural number. The content of a word \(w\) over the alphabet \(\{0, \dots, r-1\}\) is the function that assigns to each letter \(i\) the number of occurrences of \(i\) in \(w\).

def wittWordContent {r : ℕ} (w : List (Fin r)) : Fin r → ℕ :=
  fun i => w.count i

Used by 11

Used byDimension of a multihomogeneous component of a free Lie algebra · Witt's formula for the number of Lyndon words of given content · Words of given content are counted by the multinomial coefficient · Lyndon words of given content · Primitive words of given content · The content of a word sums to its length · Content is additive under concatenation · Content of a word after prepending a letter · Content of a one-letter word · Words with prescribed content · Trudi's partition sum as a sum over compositions

DefinitionLyndon word#✓fully proved

Let \(\alpha\) be a linearly ordered alphabet, and order the words over \(\alpha\) lexicographically. A word \(w\) over \(\alpha\) of length \(n\) is a Lyndon word if it is nonempty and, for every \(k\) with \(0 < k < n\), \(w\) is strictly smaller than its rotation by \(k\), the word obtained by moving the first \(k\) letters of \(w\) to the end.

def IsLyndonWord {α : Type*} [LinearOrder α] (w : List α) : Prop :=
  w ≠ [] ∧ ∀ k, 0 < k → k < w.length → w < w.rotate k

Used by 4

Used byDimension of a multihomogeneous component of a free Lie algebra · Witt's formula for the number of Lyndon words of given content · Lyndon words are primitive · Lyndon words of given content

TheoremContent is additive under concatenation#✓fully proved

For a natural number \(r\), words \(u\) and \(v\) over the alphabet \(\{0, \dots, r-1\}\), and every letter \(i\), the number of occurrences of \(i\) in the concatenation \(uv\) is the number of occurrences of \(i\) in \(u\) plus the number of occurrences of \(i\) in \(v\).

@[simp]
theorem wittWordContent_append {r : ℕ} (u v : List (Fin r)) :
    wittWordContent (u ++ v) = fun i => wittWordContent u i + wittWordContent v i

Uses 1 · Used by 2

Statement usesContent of a word

Used byDimension of a multihomogeneous component of a free Lie algebra · Witt's formula for the number of Lyndon words of given content

TheoremContent of a one-letter word#✓fully proved

Let \(r\) be a natural number. For every letter \(i\) of the alphabet \(\{0, \dots, r-1\}\), the content of the one-letter word \(i\) takes the value \(1\) at \(i\) and the value \(0\) at every other letter.

@[simp]
theorem wittWordContent_singleton {r : ℕ} (i : Fin r) :
    wittWordContent [i] = Function.update (fun _ => 0) i 1

Uses 1 · Used by 1

Statement usesContent of a word

Used byDimension of a multihomogeneous component of a free Lie algebra

TheoremContent of a word after prepending a letter#✓fully proved

Let \(r\) be a natural number, let \(w\) be a word over the alphabet \(\{0, \dots, r-1\}\), let \(i\) be a letter, and write \(c(u)\) for the content of a word \(u\) (the number of occurrences of each letter in \(u\)). If \(iw\) denotes \(w\) with \(i\) prepended, then \(c(iw)(i) = c(w)(i) + 1\) and \(c(iw)(j) = c(w)(j)\) for every letter \(j \ne i\).

@[simp]
theorem wittWordContent_cons {r : ℕ} (i : Fin r) (w : List (Fin r)) :
    wittWordContent (i :: w) =
      Function.update (wittWordContent w) i (wittWordContent w i + 1)

Uses 1 · Used by 1

Statement usesContent of a word

Used byWords of given content are counted by the multinomial coefficient

TheoremThe content of a word sums to its length#✓fully proved

For a natural number \(r\) and a word \(w\) over the alphabet \(\{0, \dots, r-1\}\), summing over all letters \(i\) the number of occurrences of \(i\) in \(w\) gives the length of \(w\).

@[simp]
theorem sum_wittWordContent {r : ℕ} (w : List (Fin r)) :
    (∑ i, wittWordContent w i) = w.length

Uses 1 · Used by 4

Statement usesContent of a word

Used byDimension of a multihomogeneous component of a free Lie algebra · Witt's formula for the number of Lyndon words of given content · Words of given content are counted by the multinomial coefficient · Trudi's partition sum as a sum over compositions

DefinitionWords with prescribed content#✓fully proved

Let \(r\) be a natural number. Given a function \(d\) from the alphabet \(\{0, \dots, r-1\}\) to the natural numbers, the words of content \(d\) are the words \(w\) over this alphabet whose content equals \(d\), that is, in which each letter \(i\) occurs exactly \(d(i)\) times.

def WordsOfContent {r : ℕ} (degree : Fin r → ℕ) :=
  {w : List (Fin r) // wittWordContent w = degree}

Uses 1 · Used by 6

Statement usesContent of a word

Used byDimension of a multihomogeneous component of a free Lie algebra · Witt's formula for the number of Lyndon words of given content · Words of given content are counted by the multinomial coefficient · Lyndon words of given content · Primitive words of given content · Trudi's partition sum as a sum over compositions

DefinitionLyndon words of given content#✓fully proved

For a natural number \(r\) and natural numbers \(n_0, \dots, n_{r-1}\), the set of Lyndon words over the alphabet \(\{0, \dots, r-1\}\), ordered as the natural numbers, in which each letter \(i\) occurs exactly \(n_i\) times.

def LyndonWordsOfContent {r : ℕ} (degree : Fin r → ℕ) :=
  {w : WordsOfContent degree // IsLyndonWord w.1}

Uses 3 · Used by 2

Statement usesLyndon word · Words with prescribed content · Content of a word

Used byDimension of a multihomogeneous component of a free Lie algebra · Witt's formula for the number of Lyndon words of given content

TheoremWords of given content are counted by the multinomial coefficient#✓fully proved

Let \(r\) be a natural number, let \(n_0, \dots, n_{r-1}\) be natural numbers, and let \(n = n_0 + \dots + n_{r-1}\). The number of words over the alphabet \(\{0, \dots, r-1\}\) in which each letter \(i\) occurs exactly \(n_i\) times is the multinomial coefficient \(\binom{n}{n_0, \ldots, n_{r-1}} = \frac{n!}{n_0! \cdots n_{r-1}!}\).

theorem card_wordsOfContent_eq_multinomial {r : ℕ} (degree : Fin r → ℕ) :
    Fintype.card (WordsOfContent degree) = Nat.multinomial Finset.univ degree

Uses 4 · Used by 2

Statement usesWords with prescribed content · The content of a word sums to its length · Content of a word

Proof usesContent of a word after prepending a letter

Used byWitt's formula for the number of Lyndon words of given content · Trudi's partition sum as a sum over compositions

TheoremPrimitivity via distinct rotations#✓fully proved

Let \(w\) be a word of length \(n\), and for \(0 \le k < n\) let \(w_k\) be the rotation of \(w\) by \(k\), obtained by moving the first \(k\) letters of \(w\) to the end. Then \(w\) is primitive if and only if \(w\) is nonempty and the \(n\) words \(w_0, w_1, \dots, w_{n-1}\) are pairwise distinct.

theorem isPrimitiveWord_iff_nodup_cyclicPermutations {α : Type*} {w : List α} :
    IsPrimitiveWord w ↔ w ≠ [] ∧ w.cyclicPermutations.Nodup

Uses 1 · Used by 3

Statement usesPrimitive word

Used byWitt's formula for the number of Lyndon words of given content · Lyndon words are primitive · Nontrivial rotations move a primitive word

TheoremNontrivial rotations move a primitive word#✓fully proved

If \(w\) is a primitive word of length \(n\) and \(0 < k < n\), then the rotation of \(w\) by \(k\), obtained by moving the first \(k\) letters of \(w\) to the end, is different from \(w\).

theorem rotate_ne_of_isPrimitiveWord {α : Type*} {w : List α}
    (hw : IsPrimitiveWord w) {k : ℕ} (hk0 : 0 < k) (hk : k < w.length) :
    w.rotate k ≠ w

Uses 2 · Used by 1

Statement usesPrimitive word

Proof usesPrimitivity via distinct rotations

Used byWitt's formula for the number of Lyndon words of given content

DefinitionPrimitive words of given content#✓fully proved

For a natural number \(r\) and natural numbers \(n_0, \dots, n_{r-1}\), the set of primitive words over the alphabet \(\{0, \dots, r-1\}\) in which each letter \(i\) occurs exactly \(n_i\) times.

def PrimitiveWordsOfContent {r : ℕ} (degree : Fin r → ℕ) :=
  {w : WordsOfContent degree // IsPrimitiveWord w.1}

Uses 3 · Used by 1

Statement usesPrimitive word · Words with prescribed content · Content of a word

Used byWitt's formula for the number of Lyndon words of given content

TheoremLyndon words are primitive#✓fully proved

Every Lyndon word over a linearly ordered alphabet is primitive.

theorem isPrimitiveWord_of_isLyndonWord {α : Type*} [LinearOrder α] {w : List α}
    (hw : IsLyndonWord w) : IsPrimitiveWord w

Uses 3 · Used by 1

Statement usesLyndon word · Primitive word

Proof usesPrimitivity via distinct rotations

Used byWitt's formula for the number of Lyndon words of given content

TheoremWitt's formula for the number of Lyndon words of given content#✓fully proved

Let \(r\) be a natural number and let \(n_0, \dots, n_{r-1}\) be natural numbers with \(n = n_0 + \dots + n_{r-1} > 0\). Order the alphabet \(\{0, \dots, r-1\}\) as the natural numbers and order words over it lexicographically. Then the number of Lyndon words over this alphabet in which each letter \(i\) occurs exactly \(n_i\) times equals, as a rational number, Witt's multigraded value \(M(n_0, \dots, n_{r-1}) = \frac{1}{n} \sum_{d \mid g} \mu(d) \binom{n/d}{n_0/d, \ldots, n_{r-1}/d}\), where \(g = \gcd(n_0, \dots, n_{r-1})\), the sum runs over the positive divisors \(d\) of \(g\), and \(\mu\) is the Möbius function.

theorem card_lyndonWordsOfContent_eq_wittMultigradedValue {r : ℕ}
    (degree : Fin r → ℕ) (hdegree : 0 < ∑ i, degree i) :
    (Fintype.card (LyndonWordsOfContent degree) : ℚ) = wittMultigradedValue degree

Uses 13 · Used by 1

Statement usesLyndon word · Lyndon words of given content · Words with prescribed content · The content of a word sums to its length · Witt's multigraded value · Content of a word

Proof usesPrimitive word · Primitive words of given content · Words of given content are counted by the multinomial coefficient · Primitivity via distinct rotations · Lyndon words are primitive · Nontrivial rotations move a primitive word · Content is additive under concatenation

Used byDimension of a multihomogeneous component of a free Lie algebra

15 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.