Documentation

Complexity.Foundations.Combinatorics.FunctionalGraph.Projection

The cycle projection and eventual behaviour #

For f on a finite type, the iterate f^[(card α)!] is an idempotent retraction onto the periodic points (cycleProjection). An orbit agrees with the orbit of its projection exactly from the transient depth on (iterate_eq_projection_iff), so questions about the eventual behaviour of an orbit become questions about one periodic orbit: whether a target recurs arbitrarily late (recurring_target_iff) or holds from some time on (eventually_always_target_iff). Two orbits meet at a common time exactly when they agree at time card α (exists_iterate_eq_iterate_iff), and every time can be replaced by one below 2 * card α (iterate_normalizedTime).

When a target is reachable, making it absorbing turns its first visit into the transient depth of the absorbing map (first_target_depth); for a map that already fixes its halting states, the first halting time is the transient depth itself (halting_depth).

The state type may live in any universe. No order on it is needed.

Main definitions #

Main results #

References #

source
theorem Cslib.FunctionalGraph.eq_of_iterate_eq_of_mem_periodicPts {α : Type u} (f : α → α) {x y : α} (hx : x ∈ Function.periodicPts f) (hy : y ∈ Function.periodicPts f) (t : ℕ) (he : f^[t] x = f^[t] y) :
x = y

Two periodic points with the same state after t steps are equal.

source
theorem Cslib.FunctionalGraph.iterate_card_mem_periodicPts {α : Type u} (f : α → α) [Fintype α] (x : α) :
f^[Fintype.card α] x ∈ Function.periodicPts f

After as many steps as there are states, every orbit is at a periodic point.

source
def Cslib.FunctionalGraph.cycleProjection {α : Type u} (f : α → α) [Fintype α] (x : α) :
α

The cycle projection f^[(card α)!]: it fixes exactly the periodic points and maps every state to a periodic point of its orbit.

Instances For
    source
    theorem Cslib.FunctionalGraph.cycleProjection_mem_periodicPts {α : Type u} (f : α → α) [Fintype α] (x : α) :
    cycleProjection f x ∈ Function.periodicPts f

    The cycle projection of every state is periodic.

    source
    theorem Cslib.FunctionalGraph.cycleProjection_eq_self_iff {α : Type u} (f : α → α) [Fintype α] (x : α) :
    cycleProjection f x = x ↔ x ∈ Function.periodicPts f

    The cycle projection fixes x exactly when x is periodic.

    source
    @[simp]
    theorem Cslib.FunctionalGraph.cycleProjection_cycleProjection {α : Type u} (f : α → α) [Fintype α] (x : α) :
    cycleProjection f (cycleProjection f x) = cycleProjection f x

    The cycle projection is idempotent.

    source
    @[simp]
    theorem Cslib.FunctionalGraph.cycleProjection_iterate {α : Type u} (f : α → α) [Fintype α] (x : α) (t : ℕ) :
    cycleProjection f (f^[t] x) = f^[t] (cycleProjection f x)

    The cycle projection commutes with iterating f.

    source
    theorem Cslib.FunctionalGraph.iterate_eq_projection_iff {α : Type u} (f : α → α) [Fintype α] (x : α) (t : ℕ) :
    f^[t] x = f^[t] (cycleProjection f x) ↔ transientDepth f x ≤ t

    Cycle entry. The orbit of x agrees with the orbit of its projection exactly from the transient depth onward.

    source
    theorem Cslib.FunctionalGraph.exists_iterate_eq_iterate_iff {α : Type u} (f : α → α) [Fintype α] (x y : α) :
    (∃ (t : ℕ), f^[t] x = f^[t] y) ↔ f^[Fintype.card α] x = f^[Fintype.card α] y

    Synchronous coalescence. Two orbits are ever in the same state at the same time exactly when they are at time card α.

    source
    noncomputable def Cslib.FunctionalGraph.normalizedTime {α : Type u} (f : α → α) [Fintype α] (x : α) (t : ℕ) :
    ℕ

    A time below 2 * card α at which the orbit of x is in the same state as at time t: t itself if it is below card α, and otherwise card α plus the remaining time modulo the cycle length.

    Instances For
      source
      theorem Cslib.FunctionalGraph.normalizedTime_lt {α : Type u} (f : α → α) [Fintype α] (x : α) (t : ℕ) :
      normalizedTime f x t < 2 * Fintype.card α

      The normalized time is less than twice the number of states.

      source
      theorem Cslib.FunctionalGraph.iterate_normalizedTime {α : Type u} (f : α → α) [Fintype α] (x : α) (t : ℕ) :
      f^[normalizedTime f x t] x = f^[t] x

      At the normalized time, the orbit of x is in the same state as at time t.

      source
      theorem Cslib.FunctionalGraph.recurring_target_iff {α : Type u} (f : α → α) [Fintype α] (P : α → Prop) (x : α) :
      (∀ (a : ℕ), ∃ (t : ℕ), a ≤ t ∧ P (f^[t] x)) ↔ ∃ (t : ℕ), P (f^[t] (cycleProjection f x))

      Recurring targets. A target is visited at arbitrarily late times exactly when the orbit of the cycle projection visits it.

      source
      theorem Cslib.FunctionalGraph.eventually_always_target_iff {α : Type u} (f : α → α) [Fintype α] (P : α → Prop) (x : α) :
      (∃ (a : ℕ), ∀ (t : ℕ), a ≤ t → P (f^[t] x)) ↔ ¬∃ (t : ℕ), ¬P (f^[t] (cycleProjection f x))

      Eventually permanent targets. A target holds from some time on exactly when the orbit of the cycle projection never leaves it.

      First visits as transient depths #

      source
      theorem Cslib.FunctionalGraph.first_target_depth {α : Type u} (f : α → α) [Finite α] (P : α → Prop) [DecidablePred P] (x : α) (h : ∃ (t : ℕ), P (f^[t] x)) :
      P (f^[transientDepth (absorb f P) x] x) ∧ ∀ j < transientDepth (absorb f P) x, ¬P (f^[j] x)

      First targets. If the orbit of x reaches P, it first does so at the transient depth of x under the map that stops at P.

      source
      theorem Cslib.FunctionalGraph.halting_depth {α : Type u} (f : α → α) [Finite α] (H : α → Prop) (hstop : ∀ (x : α), H x → f x = x) (x : α) (h : ∃ (t : ℕ), H (f^[t] x)) :
      H (f^[transientDepth f x] x) ∧ ∀ j < transientDepth f x, ¬H (f^[j] x)

      Halting depth. If f fixes every halting state and the orbit of x halts, it first halts at the transient depth of x.