Let $f : \mathbb S^1 \to \mathbb S^1$ be an orientation-preserving homeomorphism. The classical definition of the rotation number is the following: we lift $f$ to a homeomorphism $F : \mathbb R \to \mathbb R$ and we define the rotation number to be $$\rho(f) =\lim_{n\to \infty} \frac{F^n(x)}{n}$$ (for a fixed point $x \in \mathbb S^1$).
Apparently an equivalent definition is the following: $$ \rho(f)= \lim_{n\to \infty} \frac{1}{n} \textrm{#}\Big \{ 0\leq i \leq n: \ f^i(x) \in [z ,f(z)) \Big\} $$ where $ x \in \mathbb{S} ^1$ and $\textrm{#}X$ denotes number elements of a set $X$.
Can you help me to prove that?
To make sure I got the terminology correctly,
I write $\rho(f)$ for the first definition and $\hat{\rho}(f)$ for the second.
Intuitively, $\rho(f)$ is the average rotation speed of the orbits of $f$. The criterion $f^i(x)\in [z,f(z))$ is an indicator that the orbit of $x$ has turned one more time around the circle at step $i$, so $\hat{\rho}(f)$ is simply the average number of turns per iteration of $f$, which is another way to measure the rotation speed.
Let us try to make this intuition precise. By subtracting a suitable integer if necessary, we can assume that $z-1<F(z)<z+1$ for every $z\in\mathbb{R}$. If $f$ has a fixed point, then every orbit is asymptotic to a fixed point of $f$, and both definitions give $0$. So, without loss of generality, we may also assume that $z<F(z)<z+1$ for every $z\in\mathbb{R}$.
Let $x,z\in\mathbb{R}$ be arbitrary. For $n\in\mathbb{N}$, define \begin{align} r_n &:= \sup\{r\in\mathbb{Z}: r+z\leq F^n(x)\} \\ &= \lfloor F^n(x) - z\rfloor \;. \end{align} Intuitively, $r_n$ is more or less the number of times the orbit of $x$ has passed $z$.
Observation. $\lim_{n\to\infty} {\displaystyle\frac{r_n}{n}} \bmod 1 = \rho(f)$.
The relationship between $r_n$ and the second definition is a consequence of the lemma below. I divide the lemma into three claims.
Claim I. $r_i\leq r_{i+1}\leq r_i+1$.
Claim II. $r_{i+1}=r_i+1$ if and only if $F^{i+1}(x)\in [\,r_{i+1}+z,r_{i+1}+F(z)\,)$.
Claim III. $F^i(x)\in[\,m+z,m+F(z)\,)$ implies $m=r_i$.
Combining the above claims, we have
Lemma. $r_i\leq r_{i+1}\leq r_i+1$, and the equality $r_{i+1}=r_i+1$ happens if and only if $f(\overline{x}) \in [\,\overline{z}, f(\overline{z})\,)$.
The above lemma immediately gives $\lim_{n\to\infty} {\displaystyle\frac{r_n}{n}} = \hat{\rho}(f)$, concluding the proof.