Phases, first hitting times, and visit schedules in finite functional graphs

Past the transient, two times give the same state exactly when they agree modulo the cycle length (iterate_eq_iterate_iff_modEq). Given a linear order on the states, every state past the transient is determined by the canonical cycle representative and its phase (iterate_eq_iterate_phase), and iterating shifts the phase (phase_iterate).

These identities give the first hitting time of any target y from x in closed form (hittingTime_spec). A periodic target is reached exactly when both have the same canonical representative, first after the transient of x and the phase difference (cyclicDistance). A transient target is reached only at the difference of the transient depths. In both cases the time is below the number of states.

After the first visit to a target, subsequent visits form an arithmetic progression with step Function.minimalPeriod f y, where period zero makes a single visit a special case of the same formula (visit_schedule_of_first, visit_schedule), and the number of visits up to a deadline T is given by arithmeticProgressionCount (visit_count_of_first).

The state type may live in any universe; it is finite, and representatives use a linear order.

Main definitions

• Cslib.FunctionalGraph.cyclicDistance: the phase difference from x to a target on its cycle.
• Cslib.FunctionalGraph.reaches: whether the orbit of x reaches y, in closed form.
• Cslib.FunctionalGraph.hittingTime: the first hitting time, in closed form.
• Cslib.FunctionalGraph.arithmeticProgressionCount: count of progression terms up to a deadline.

Main results

• Cslib.FunctionalGraph.iterate_eq_iterate_phase: states past the transient by phase.
• Cslib.FunctionalGraph.phase_iterate: iterating shifts the phase.
• Cslib.FunctionalGraph.cyclic_first_hit: the first hit of a periodic target.
• Cslib.FunctionalGraph.reaches_iff, Cslib.FunctionalGraph.hittingTime_spec: reachability and the exact first hitting time.
• Cslib.FunctionalGraph.visit_schedule_of_first, Cslib.FunctionalGraph.visit_before_deadline_of_first, Cslib.FunctionalGraph.visit_schedule: complete schedules of visits.
• Cslib.FunctionalGraph.arithmeticProgressionCount_spec, Cslib.FunctionalGraph.visit_count_of_first: counting visits up to a deadline.

References

• Adapted from lean/Proofs/{HittingTimes,Navigation,VisitSchedules,VisitCounts}.lean in S. Schlesinger, Square-root circuit bounds for iterated functions.

theorem Cslib.FunctionalGraph.iterate_mem_cycleSet {α : Type u} [Finite α] (f : α → α) {x : α} (hx : x ∈ Function.periodicPts f) (j : ℕ) : f^[j] x ∈ cycleSet f x

Every state of the orbit of a periodic state lies on its cycle.

theorem Cslib.FunctionalGraph.phase_add_canonicalTime_modEq {α : Type u} [Finite α] (f : α → α) [LinearOrder α] (x : α) : phase f x + canonicalTime f x ≡ 0 [MOD cycleLength f x]

The phase cancels the time of the first visit to the representative.

theorem Cslib.FunctionalGraph.iterate_eq_iterate_phase {α : Type u} [Finite α] (f : α → α) [LinearOrder α] (x : α) {t : ℕ} (ht : transientDepth f x ≤ t) : f^[t] x = f^[(phase f x + t) % cycleLength f x] (canonicalCycle f x)

Past the transient, the state is the representative advanced by the phase plus the time.

theorem Cslib.FunctionalGraph.phase_eq_of_iterate_eq_canonicalCycle {α : Type u} [Finite α] (f : α → α) [LinearOrder α] (x : α) {t : ℕ} (ht : f^[t] x = canonicalCycle f x) : phase f x = (cycleLength f x - t % cycleLength f x) % cycleLength f x

Any visit to the representative determines the phase.

@[simp]

theorem Cslib.FunctionalGraph.phase_iterate {α : Type u} [Finite α] (f : α → α) [LinearOrder α] (x : α) (t : ℕ) : phase f (f^[t] x) = (phase f x + t) % cycleLength f x

Iterating shifts the phase by the number of steps.

noncomputable def Cslib.FunctionalGraph.cyclicDistance {α : Type u} [Finite α] (f : α → α) [LinearOrder α] (x y : α) : ℕ

The number of steps after the transient of x to a target on the same cycle: the phase difference modulo the cycle length.

theorem Cslib.FunctionalGraph.cyclic_first_hit {α : Type u} [Finite α] (f : α → α) [LinearOrder α] (x y : α) (hy : y ∈ Function.periodicPts f) (hc : canonicalCycle f x = canonicalCycle f y) : f^[transientDepth f x + cyclicDistance f x y] x = y ∧ ∀ j < transientDepth f x + cyclicDistance f x y, f^[j] x ≠ y

First hit of a periodic target. If y is periodic with the same canonical representative as x, the orbit of x first reaches y after its transient and the cyclic distance.

noncomputable def Cslib.FunctionalGraph.reaches {α : Type u} [Finite α] (f : α → α) [LinearOrder α] (x y : α) : Bool

Whether the orbit of x reaches y: for a periodic target, whether both have the same canonical representative; for a transient target, whether the state at the difference of the transient depths is y.

noncomputable def Cslib.FunctionalGraph.hittingTime {α : Type u} [Finite α] (f : α → α) [LinearOrder α] (x y : α) : ℕ

The first hitting time from x to y when y is reachable: the transient and the cyclic distance for a periodic target, the difference of the transient depths otherwise.

theorem Cslib.FunctionalGraph.reaches_iff {α : Type u} [Finite α] (f : α → α) [LinearOrder α] (x y : α) : reaches f x y = true ↔ ∃ (t : ℕ), f^[t] x = y

reaches f x y holds exactly when the orbit of x visits y.

theorem Cslib.FunctionalGraph.hittingTime_spec {α : Type u} [Finite α] (f : α → α) [LinearOrder α] [Fintype α] (x y : α) (h : reaches f x y = true) : f^[hittingTime f x y] x = y ∧ (∀ j < hittingTime f x y, f^[j] x ≠ y) ∧ hittingTime f x y < Fintype.card α

First hitting times. If y is reachable from x, then hittingTime f x y is the first time the orbit of x visits y, and it is below the number of states. Nothing is claimed about hittingTime f x y when y is unreachable.

Complete visit schedules and bounded visit counts

theorem Cslib.FunctionalGraph.visit_schedule_of_first {α : Type u} (f : α → α) (x y : α) (d : ℕ) (hd : f^[d] x = y) (hfirst : ∀ j < d, f^[j] x ≠ y) (t : ℕ) : f^[t] x = y ↔ ∃ (k : ℕ), t = d + k * Function.minimalPeriod f y

After the first visit to y at time d, subsequent visits form an arithmetic progression with step Function.minimalPeriod f y, where period zero makes a single visit a special case of the same formula.

theorem Cslib.FunctionalGraph.visit_before_deadline_of_first {α : Type u} (f : α → α) (x y : α) (d : ℕ) (hd : f^[d] x = y) (hfirst : ∀ j < d, f^[j] x ≠ y) (T : ℕ) : (∃ t ≤ T, f^[t] x = y) ↔ d ≤ T

When d is the first visit time to y, a visit occurs on or before T iff d ≤ T.

theorem Cslib.FunctionalGraph.visit_schedule {α : Type u} [Finite α] (f : α → α) [LinearOrder α] (x y : α) (t : ℕ) : f^[t] x = y ↔ reaches f x y = true ∧ ∃ (k : ℕ), t = hittingTime f x y + k * Function.minimalPeriod f y

Complete visit schedule from x to y in terms of reaches, hittingTime, and Function.minimalPeriod.

def Cslib.FunctionalGraph.arithmeticProgressionCount (d p T : ℕ) : ℕ

Number of progression terms d + k * p in {0, ..., T}, with p = 0 denoting a singleton visit at d.

theorem Cslib.FunctionalGraph.arithmeticProgressionCount_spec (d p T : ℕ) : {t : ℕ | t ≤ T ∧ ∃ (k : ℕ), t = d + k * p}.ncard = arithmeticProgressionCount d p T

arithmeticProgressionCount d p T counts the times t ≤ T of the form d + k * p.

theorem Cslib.FunctionalGraph.visit_count_of_first {α : Type u} (f : α → α) (x y : α) (d : ℕ) (hd : f^[d] x = y) (hfirst : ∀ j < d, f^[j] x ≠ y) (T : ℕ) : {t : ℕ | t ≤ T ∧ f^[t] x = y}.ncard = arithmeticProgressionCount d (Function.minimalPeriod f y) T

Number of visits from x to y up to time T when d is the first visit time.