The number of distinct powers of a finite map

For f : α → α on a finite type, let μ be the longest transient depth (maxTransientDepth) and λ the least common multiple of the cycle lengths (cyclePeriod). Two powers f^[a] and f^[b] with a < b agree exactly when μ ≤ a and λ ∣ b - a (iterate_eq_iterate_iff), so f has exactly μ + λ distinct powers (card_range_iterate). On an empty type μ = 0 and λ = 1: the only power is the empty function.

Main definitions

• Cslib.FunctionalGraph.maxTransientDepth: the longest transient depth μ.
• Cslib.FunctionalGraph.cyclePeriod: the least common multiple λ of the cycle lengths.

Main results

• Cslib.FunctionalGraph.iterate_eq_iterate_iff: when two powers agree.
• Cslib.FunctionalGraph.iterate_eq_iterate_reduce: every power is one of the first μ + λ.
• Cslib.FunctionalGraph.card_range_iterate: exactly μ + λ distinct powers.

References

• Adapted from lean/Proofs/NumberOfPowers.lean in S. Schlesinger, Square-root circuit bounds for iterated functions.

noncomputable def Cslib.FunctionalGraph.maxTransientDepth {α : Type u} [Fintype α] (f : α → α) : ℕ

The longest transient depth μ over all states.

noncomputable def Cslib.FunctionalGraph.cyclePeriod {α : Type u} [Fintype α] (f : α → α) : ℕ

The least common multiple λ of all cycle lengths.

theorem Cslib.FunctionalGraph.cyclePeriod_pos {α : Type u} [Fintype α] (f : α → α) : 0 < cyclePeriod f

The least common multiple of all cycle lengths is positive.

theorem Cslib.FunctionalGraph.iterate_eq_iterate_iff {α : Type u} [Fintype α] (f : α → α) {a b : ℕ} (hab : a < b) : f^[a] = f^[b] ↔ maxTransientDepth f ≤ a ∧ cyclePeriod f ∣ b - a

Two powers f^[a] and f^[b] with a < b coincide iff μ ≤ a and λ ∣ b - a.

theorem Cslib.FunctionalGraph.iterate_eq_iterate_reduce {α : Type u} [Fintype α] (f : α → α) {T : ℕ} (hT : maxTransientDepth f ≤ T) : f^[T] = f^[maxTransientDepth f + (T - maxTransientDepth f) % cyclePeriod f]

Every power past μ reduces to one of the first μ + λ powers.

theorem Cslib.FunctionalGraph.iterate_injective_below {α : Type u} [Fintype α] (f : α → α) : Function.Injective fun (i : Fin (maxTransientDepth f + cyclePeriod f)) => f^[↑i]

The powers f^[0], …, f^[μ + λ - 1] are pairwise distinct.

theorem Cslib.FunctionalGraph.card_range_iterate {α : Type u} [Fintype α] (f : α → α) : Nat.card ↑(Set.range fun (T : ℕ) => f^[T]) = maxTransientDepth f + cyclePeriod f

The number of powers. A map on a finite type has exactly μ + λ distinct powers.