\section{Diophantine approximation}\label{sec:diophapprox}

The following result is often stated with the condition that $Q$
be an integer. Let us prove it for all real $Q\geq 1$. (This variant
is of course
well-known.)

\begin{lemma}[Dirichlet's approximation theorem]\label{lem:dirithm}\index{Dirichlet's approximation theorem|boldindex}
  Let $\alpha\in \mathbb{R}$, $Q\geq 1$. Then there are integers $a$,
  $1\leq q\leq Q$ with $(a,q)=1$ such that
  \begin{equation}\label{eq:kukulir}
    \left|\alpha - \frac{a}{q}\right|< \frac{1}{q Q}.\end{equation}
\end{lemma}
If only a non-strict inequality $\leq$ is desired in (\ref{eq:kukulir}),
the proof below can be modified so as to give a strict inequality for $q$,
that is, $q<Q$.
\begin{proof}
  Let $m = \lfloor Q\rfloor$. Consider the following $m+1$ points
  in the circle $\mathbb{R}/\mathbb{Z}$:
  \[0\cdot \alpha,
  1\cdot \alpha, \dotsc, m\cdot \alpha\; \mo \mathbb{Z}.\] 
  At least two of them must be at distance 
  no more than $1/(m+1)$ from each other. Call them $b_1 \alpha \mo \mathbb{Z}$,
  $b_2 \alpha \mo \mathbb{Z}$,
  $b_1<b_2$. Then
  \[d((b_2 - b_1) \alpha,\mathbb{Z}) = d(b_2 \alpha - b_1 \alpha,\mathbb{Z})\leq
  \frac{1}{m+1} < \frac{1}{Q},\]
  i.e., there is an integer $a$ such that $|(b_2 - b_1) \alpha - a|<1/Q$.
  Define $q = b_2 - b_1$. Then $|\alpha - a/q|<1/q Q$. If $a$, $q$ are not
  coprime, divide both of them by $(a,q)$.
\end{proof}

\begin{lemma}\label{lem:hardio}
  Let $\alpha\in \mathbb{R}$. Let $a$ and $q\geq 1$ be coprime integers such that
  $\epsilon = |\alpha - a/q|$ satisfies $0<\epsilon\leq 1/q^2$.
  Then, for $Q = 1/\epsilon q$, there exist coprime integers $a'$, $q'$ such that
  \[\left|\alpha - \frac{a'}{q'}\right|\leq \frac{1}{q' Q}\;\;\;\;\;\;
  \text{and}\;\;\;\;\;\;\frac{Q}{2} < q'\leq Q.\]
\end{lemma}
\begin{proof}
  By the definition of $\epsilon$ and $Q$, we have $|\alpha - a/q|=\epsilon=1/q Q$.
  Since $\epsilon\leq 1/q^2$, we see that $q\leq Q$. 
Dirichlet's approximation theorem (Lem.~\ref{lem:dirithm}) assures us
that there exist coprime integers $a_1$, $1\leq q_1\leq Q$ such that
$|\alpha - a_1/q_1|<1/q_1 Q$. Then $a/q \ne a_1/q_1$, and so
\[\left|\frac{a}{q} - \frac{a_1}{q_1}\right|\geq \frac{1}{q q_1}.\]

At the same time, 
\[\left|\frac{a}{q} - \frac{a_1}{q_1}\right|\leq
\left|\alpha - \frac{a}{q}\right| + \left|\alpha - \frac{a_1}{q_1}\right|<
\frac{1}{q Q} + \frac{1}{q_1 Q}.\]
Hence $1/q Q + 1/q_1 Q > 1/q q_1$, and
so $q + q_1 > Q$.
If $q_1> Q/2$, let $a'/q' = a_1/q_1$. If $q_1\leq Q/2$, then $q>Q/2$,
and we may let $a'/q' = a/q$.
\end{proof}