Simulating the iterates of one function by another

Read f : α → α and g : β → β as the one-step transitions of two discrete-time systems and Φ : α → β as a translation of the states of the first into states of the second. Say that g simulates f along Φ when every single step of f is matched by finitely many steps of g on the translated states. TauCeti.exists_iterate_of_forall_exists_iterate says that a simulation of the single steps is automatically a simulation of all the iterates, so a run of f of any length may be replayed as a run of g.

This is the form in which a coarse system is compared with a finer one that refines each of its steps into a finite stretch of its own, of a length that may vary from state to state: only the single steps have to be inspected, and the lengths of the stretches never have to be tracked.

Main results

• TauCeti.exists_iterate_of_forall_exists_iterate: a simulation of single steps is a simulation of iterates.

theorem TauCeti.exists_iterate_of_forall_exists_iterate {α : Type u_1} {β : Type u_2} {f : α → α} {g : β → β} {Φ : α → β} (h : ∀ (a : α), ∃ (m : ℕ), g^[m] (Φ a) = Φ (f a)) (n : ℕ) (a : α) : ∃ (m : ℕ), g^[m] (Φ a) = Φ (f^[n] a)

If every step of f is simulated by finitely many steps of g along Φ, then so is every iterate of f.