Eventually periodic sequences

DefinitionEventually periodic sequences#✓fully proved

A sequence \(u : \mathbb{N} \to \alpha\) with values in a type \(\alpha\) is eventually periodic if there are natural numbers \(p > 0\) (a period) and \(n_0\) (a preperiod) such that \(u(n + p) = u(n)\) for every natural number \(n \ge n_0\).

def IsEventuallyPeriodic {α : Type _} (u : ℕ → α) : Prop :=
  ∃ p n₀ : ℕ, 0 < p ∧ ∀ n : ℕ, n₀ ≤ n → u (n + p) = u n

Used by 14

Used byPansiot's classification of the factor complexity of pure morphic words · Ultimately periodic sequences · Orbits in a finite set are eventually periodic · Periodic sequences are eventually periodic · Explicit period and preperiod give eventual periodicity · Period and preperiod of an eventually periodic sequence · Lagrange's theorem for Mallows representations · Mallows and Stern–Brocot representations are eventually periodic together · Typical properties of Mallows representations · Eventually periodic continued fractions · Lagrange's theorem on periodic continued fractions · Euler's theorem on periodic continued fractions · P-recursive sequences with leading coefficient 1 are MC-finite · Polynomial recursions give MC-finite sequences

TheoremExplicit period and preperiod give eventual periodicity#✓fully proved

Let \(\alpha\) be a type and \(u : \mathbb{N} \to \alpha\) a sequence. If there are natural numbers \(p > 0\) and \(n_0\) such that \(u(n + p) = u(n)\) for every natural number \(n \ge n_0\), then \(u\) is eventually periodic.

theorem IsEventuallyPeriodic.of_witness {α : Type _} {u : ℕ → α} {p n₀ : ℕ}
    (hp : 0 < p) (h : ∀ n : ℕ, n₀ ≤ n → u (n + p) = u n) :
    IsEventuallyPeriodic u

Uses 1 · Used by 1

Statement usesEventually periodic sequences

Used byLagrange's theorem on periodic continued fractions

TheoremPeriod and preperiod of an eventually periodic sequence#✓fully proved

Let \(\alpha\) be a type. If a sequence \(u : \mathbb{N} \to \alpha\) is eventually periodic, then there are natural numbers \(p > 0\) and \(n_0\) such that \(u(n + p) = u(n)\) for every natural number \(n \ge n_0\).

theorem IsEventuallyPeriodic.witness_spec {α : Type _} {u : ℕ → α}
    (h : IsEventuallyPeriodic u) :
    ∃ p n₀ : ℕ, 0 < p ∧ ∀ n : ℕ, n₀ ≤ n → u (n + p) = u n

Uses 1

Statement usesEventually periodic sequences

TheoremPeriodic sequences are eventually periodic#✓fully proved

Let \(\alpha\) be a type, let \(u : \mathbb{N} \to \alpha\) be a sequence and let \(p > 0\) be a natural number with \(u(n + p) = u(n)\) for every \(n \in \mathbb{N}\). Then \(u\) is eventually periodic.

theorem IsEventuallyPeriodic.of_periodic {α : Type _} {u : ℕ → α} {p : ℕ}
    (hp : 0 < p) (h : ∀ n : ℕ, u (n + p) = u n) : IsEventuallyPeriodic u

Uses 1 · Used by 1

Statement usesEventually periodic sequences

Used byP-recursive sequences with leading coefficient 1 are MC-finite

AbbreviationUltimately periodic sequences#✓fully proved

Let \(\alpha\) be a type. A sequence \(u : \mathbb{N} \to \alpha\) is called ultimately periodic exactly when it is eventually periodic; the two terms name the same notion.

abbrev IsUltimatelyPeriodic {α : Type _} (u : ℕ → α) : Prop :=
  IsEventuallyPeriodic u

Uses 1 · Used by 2

Statement usesEventually periodic sequences

Used byCobham's theorem for characteristic sequences · Ultimately periodic sets and their characteristic sequences

TheoremOrbits in a finite set are eventually periodic#✓fully proved

Let \(S\) be a finite set, \(F : S \to S\) a map and \(r : \mathbb{N} \to S\) a sequence with \(r(n + 1) = F(r(n))\) for every \(n \in \mathbb{N}\). Then \(r\) is eventually periodic.

theorem IsEventuallyPeriodic.of_finite_orbit {S : Type*} [Finite S] (F : S → S) (r : ℕ → S)
    (h : ∀ n, r (n + 1) = F (r n)) : IsEventuallyPeriodic r

Uses 1 · Used by 3

Statement usesEventually periodic sequences

Used byLagrange's theorem on periodic continued fractions · P-recursive sequences with leading coefficient 1 are MC-finite · Polynomial recursions give MC-finite sequences

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.