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

\begin{lemma}[Dirichlet's approximation theorem]\label{lem:ch22dirithm}
  Let $\alpha, Q\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}
\begin{proof}
This is a standard form of Dirichlet's approximation theorem.
You may deduce it from any suitable version already available in Mathlib.
\end{proof}

\begin{lemma}\label{lem:ch22diffrac}
Let $a_1$, $a_2$, $q_1\geq 1$ and $q_2\geq 1$ be positive integers. If
$a_1/q_1\ne a_2/q_2$, then $|a_1/q_1-a_2/q_2|\geq 1/(q_1 q_2)$.
\end{lemma}
\begin{proof}
We can write $a_1/q_1 - a_2/q_2 = (a_1 q_2 - a_2 q_1)/(q_1 q_2)$. If
$a_1 q_2 - a_2 q_1$ were $0$, then $a_1/q_1-a_2/q_2$ would be $0$, but, by
assumption, it is not. Hence, since $a_1 q_2 - a_2 q_1$ is an integer,
and non-zero, it must have absolute value $\geq 1$. The conclusion follows.
\end{proof}

\begin{lemma}\label{lem:ch22hardio}
  Let $\alpha\in \mathbb{R}$. Let $a$ and $q\geq 1$ be coprime integers such that $0<|\alpha-a/q|\leq 1/q^2$. Let $Q\in \mathbb{R}$ be such that
$|\alpha-a/q| = 1/(q Q)$. Then  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}
  Since $1/(q Q)\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, by Lemma
\ref{lem:ch22diffrac},
\[\left|\frac{a}{q} - \frac{a_1}{q_1}\right|\geq \frac{1}{q q_1}.\]

At the same time, by the triangle inequality and the bounds on
$|\alpha-a/q|$ and $|\alpha-a_1/q_1|$ we have just proven,
\[\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)$. Since $q,q_1>0$ and $Q>0$, 
multiplying both sides by $q q_1 Q$ preserves the inequality, and we obtain
that  $q_1 + q > Q$.

We have two cases.
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}