An equivalent definition of the rotation number of a circle homeomorphism 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?
 A: To make sure I got the terminology correctly,


*

*I assume the lifting is given by the standard projection $x\mapsto x \bmod 1$, so $F(x)\bmod 1=f(x\bmod 1)$.  For brevity, I will denote $x\bmod 1$ by $\overline{x}$.

*I assume orientation-preserving means the lifting $F$ can be chosen to be an increasing function.


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$.  

Argument. By definition, $r_i+z\leq F^i(x)<r_i+1+z$.
  By the monotonicity of $F$, we get
    \begin{align}
     r_i+F(z) &\leq F^{i+1}(x) < r_i+1+z + \left(F(z)-z)\right) \;.
  \end{align}
  The left-hand inequality, together with $z<F(z)$ gives $r_i\leq r_{i+1}$.
  The right-hand inequality, along with $F(z)-z<1$ implies
  $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)\,)$.  

Argument.
  We have $r_{i+1}=r_i+1$ if and only if
    \begin{align}
      F^i(x) &< r_{i+1} + z \leq F^{i+1}(x) \;.
  \end{align}
  Applying $F$ and using its monotonicity, the left-hand inequality
  is equivalent to
    \begin{align}
      F^{i+1}(x) &< r_{i+1} + F(z) \;.
  \end{align}
  Therefore, $r_{i+1}=r_i+1$ if and only if
    \begin{align}
      r_{i+1} + z &\leq F^{i+1}(x) < r_{i+1} + F(z) \;.
  \end{align}

Claim III. $F^i(x)\in[\,m+z,m+F(z)\,)$ implies $m=r_i$.  

Argument. The assumption $m+z\leq F^i(x)$ implies $m\leq r_i$.
  On the other hand, $F^i(x)<m+F(z)$ and $F(z)<z+1$ give
  $F^i(x)<m+1+z$, which implies $r_i\leq m$.

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.
