iterates of function with finite domain

Stream: Is there code for X?

[Siddharth Bhat]

Let $f : A \to A$ be a function with $|A| = n$. I want to show that if $f^N(x_0) = y$ for $N > |A|$, then there must be a $k < N$ such that $f^k(x) = y$. Does this exist in mathlib?

The proof that I would perform on paper is to build a graph with $A$ as the vertex set, and $(a, a') \in E$ iff $f(a') = a$.
Then what we have is a path $p \equiv [x_0, f(x_0), f^2(x_0), \dots, f^N(x_0) = y]$. We can thus find a simple path $p'$ of length $k < N$ from the starting vertex $x_0$ to $y$ by deleting cycles. But this requires a passage through graphs that I am hoping to avoid.

[Ruben Van de Velde]

It seems plausible, stated with docs#Nat.iterate

[Siddharth Bhat]

Right, I found Nat.iterate, but it's super unclear to me how to actually prove it without building the graph and talking about paths and simple paths :sweat_smile: I feel like there is a simple pigenhole like proof I am missing.

[Ruben Van de Velde]

Oh, unless docs#Function.IsPeriodicPt is what you're looking for

[Siddharth Bhat]

Sadly not, that requires me to recur to the starting point $x$

[Siddharth Bhat]

I want to reach an arbitrary point $y$

[Damiano Testa]

Those would be called "pre-periodic" points in maths.

[Siddharth Bhat]

Aha, I may have more luck if I look for generic facts about endomorphisms.

[Siddharth Bhat]

Hm, no such luck.

[Dan Velleman]

Siddharth Bhat said:

I feel like there is a simple pigenhole like proof I am missing.

Can't you use pigeonhole to argue that $x_0, f(x_0), f^2(x_0), \ldots, f^N(x_0)$ cannot all be distinct? So there are $i$ and $j$ with $i < j \le N$ such that $f^i(x_0) = f^j(x_0)$. Then prove by induction that for all $N \ge j$, there is some $k < j$ such that $f^N(x_0) = f^k(x_0)$.

[Siddharth Bhat]

Yes, I believe this will work :) I guess I now need to find pigeonhole in mathlib?

[Timo Carlin-Burns]

docs#Fintype.exists_ne_map_eq_of_card_lt is one version of pigeonhole