Preperiodic points and grand orbits

DefinitionForward orbit#✓fully proved

For a self-map \(f\) of a set \(X\) and a point \(x \in X\), the forward orbit of \(x\) under \(f\) is the set \(\{f^n(x) : n \in \mathbb{N}\}\) of all iterates of \(x\), including \(f^0(x) = x\).

def forwardOrbit (f : α → α) (x : α) : Set α :=
  Set.range fun n : ℕ => f^[n] x

Used by 1

Used byPreperiodic point

DefinitionPreperiodic point#✓fully proved

A point \(x\) is preperiodic for a self-map \(f\) when its forward orbit \(\{f^n(x) : n \in \mathbb{N}\}\) under \(f\) is a finite set.

def IsPreperiodicPt (f : α → α) (x : α) : Prop :=
  (forwardOrbit f x).Finite

Uses 1 · Used by 1

Statement usesForward orbit

Used byStrictly preperiodic point

DefinitionStrictly preperiodic point#✓fully proved

A point \(x\) is strictly preperiodic for a self-map \(f\) when it is preperiodic for \(f\) but not periodic, that is, there is no \(n > 0\) with \(f^n(x) = x\).

def IsStrictlyPreperiodicPt (f : α → α) (x : α) : Prop :=
  IsPreperiodicPt f x ∧ x ∉ periodicPts f

Uses 1

Statement usesPreperiodic point

DefinitionPreperiodic point of a given type#✓fully proved

Let \(f\) be a self-map of a set \(X\) and let \(m\) and \(n\) be natural numbers. A point \(x \in X\) is preperiodic of type \((m, n)\) when \(n > 0\) and \(f^{m+n}(x) = f^m(x)\), that is, \(f^m(x)\) is periodic with period \(n\). Neither \(m\) nor \(n\) is required to be minimal.

def IsPreperiodicPtOfType (f : α → α) (m n : ℕ) (x : α) : Prop :=
  0 < n ∧ f^[m + n] x = f^[m] x

DefinitionGrand orbit relation#✓fully proved

For a self-map \(f\) of a set \(X\), points \(x, y \in X\) are related, that is, lie in the same grand orbit of \(f\), when \(f^m(x) = f^n(y)\) for some natural numbers \(m\) and \(n\).

def GrandOrbitRel (f : α → α) (x y : α) : Prop :=
  ∃ m n : ℕ, f^[m] x = f^[n] y

Used by 2

Used byGrand orbit · Grand orbit equivalence relation

DefinitionGrand orbit equivalence relation#✓fully proved

For a self-map \(f\) of a set \(X\), the relation on \(X\) in which \(x \sim y\) when \(f^m(x) = f^n(y)\) for some natural numbers \(m\) and \(n\) is an equivalence relation; its equivalence classes are the grand orbits of \(f\).

def grandOrbitSetoid (f : α → α) : Setoid α where
  r := GrandOrbitRel f
  iseqv := grandOrbitRel_equivalence f

Uses 1

Statement usesGrand orbit relation

DefinitionGrand orbit#✓fully proved

For a self-map \(f\) of a set \(X\) and a point \(x \in X\), the grand orbit of \(x\) is the set of all \(y \in X\) such that \(f^m(x) = f^n(y)\) for some natural numbers \(m\) and \(n\), that is, the equivalence class of \(x\) under the grand orbit relation.

def grandOrbit (f : α → α) (x : α) : Set α :=
  {y | GrandOrbitRel f x y}

Uses 1

Statement usesGrand orbit relation

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.