Documentation

Mathlib.Data.List.PeriodicityLemma

Periods of words (Lists) #

This file defines the notion of a period of a word (list) and proves the Periodicity Lemma.

Implementation notes #

The definition of a period is given in terms of self-overlap. Equivalent characterizations in terms of indices and modular arithmetic are also provided.

Tags #

periodicity lemma, Fine-Wilf theorem, period, periodicity

source
def List.HasPeriod {α : Type u_1} (w : List α) (p : ℕ) :
Prop

HasPeriod w p, means that the list w has the period p, which can be seen in two equivalent ways: · The list w starts again after the prefix of length p. That is, w overlaps with itself with offset p. · The element of w at index i is the same as the element at index i + p, for all i The definition is given in terms of the self-overlap.

Equations
Instances For
    source
    theorem List.hasPeriod_iff_getElem? {α : Type u_1} {p : ℕ} {w : List α} :
    w.HasPeriod p ↔ ∀ i < w.length - p, w[i]? = w[i + p]?

    This is the equivalent definition of HasPeriod w p by indices.

    source
    @[simp]
    theorem List.hasPeriod_zero {α : Type u_1} (w : List α) :
    w.HasPeriod 0
    source
    @[simp]
    theorem List.hasPeriod_of_length_le {α : Type u_1} (w : List α) (p : ℕ) (large : w.length ≤ p) :
    w.HasPeriod p
    source
    theorem List.hasPeriod_empty {α : Type u_1} (p : ℕ) :
    [].HasPeriod p
    source
    @[irreducible]
    theorem List.HasPeriod.getElem?_mod {α : Type u_1} (p i : ℕ) (w : List α) (per : w.HasPeriod p) (less : i < w.length) :
    w[i % p]? = w[i]?
    source
    theorem List.hasPeriod_iff_forall_getElem?_mod {α : Type u_1} {p : ℕ} {w : List α} :
    w.HasPeriod p ↔ ∀ i < w.length, w[i]? = w[i % p]?

    An equivalent definition of HasPeriod w p by modular equivalence on indices.

    source
    theorem List.HasPeriod.factor {α : Type u_1} {u v w : List α} {p : ℕ} (per : (u ++ v ++ w).HasPeriod p) :
    v.HasPeriod p

    If w has a period p, then any of its factors has a period p as well.

    source
    theorem List.HasPeriod.infix {α : Type u_1} {u w : List α} {p : ℕ} (per : w.HasPeriod p) (h : u <:+: w) :
    u.HasPeriod p
    source
    theorem List.HasPeriod.drop_prefix {α : Type u_1} {w : List α} (p : ℕ) (per : w.HasPeriod p) :
    drop p w <+: w
    source
    theorem List.HasPeriod.take_append {α : Type u_1} (p n : ℕ) (w : List α) (dvd : p ∣ n) (len : n ≤ w.length) (per : w.HasPeriod p) :
    (take n w ++ w).HasPeriod p

    If w has a period p, and we extend it to the left by its prefix whose length divides p, then the resulting word also has a period p.

    source
    theorem List.HasPeriod.drop_of_hasPeriod_add {α : Type u_1} {q k : ℕ} {w : List α} (per_q : w.HasPeriod q) (per_plus : w.HasPeriod (k + q)) :
    (drop q w).HasPeriod k

    Induction step for the periodicity_lemma

    source
    @[irreducible]
    theorem List.HasPeriod.gcd {α : Type u_1} {w : List α} {p q : ℕ} (per_p : w.HasPeriod p) (per_q : w.HasPeriod q) (len : p + q - p.gcd q ≤ w.length) :
    w.HasPeriod (p.gcd q)

    The Periodicity Lemma, also known as the Fine and Wilf theorem, shows that if word w of length at least p + q - gcd p q has two periods p and q, then it has a period gcd p q. The proof is similar to the Euclidean algorithm for computing gcd.