Asymptotic expansion for $a_n=\inf_{1\leq k \leq n}|\sin(k)|$ Can we obtain an asymptotic formula for sequences $$a_n=\inf_{1\leq k \leq n}|\sin(k)|,\ b_n=\sup_{1\leq k \leq n}|\sin(k)|$$ Moreover, what will the asymptotic formula be if we replace $\sin(x)$ by other trigonometric functions like:$$\cos(x), \tan(x), \cot(x), \sec(x), \csc(x)$$ This problem is simply out of interest, I'm not sure whether it's an open problem or not. Any kind of suggestions or references are welcomed. Thank you!
 A: This is related to the question of determining the irrationality measure of $\pi$.
For $a_n = \inf_{1 \leq k \leq n} |\sin(k)|$, we have
$$n^{-49} \leq a_n \leq n^{-1 + \epsilon} \,,$$
for $n$ sufficiently large, and if the irrationality measure of $\pi$ is $2$, then the exponent on the left can be replaced by $-1-\epsilon$.
Similar bounds hold for $b_n$, $\inf_{1 \leq k \leq n} |\cos(k)|$, $\inf_{1 \leq k \leq n} |\tan(k)|$ etc. The additional difficulty here is that the problem is related to rational approximations to $\pi$ with congruence conditions on the numerators and denominators. The (very short) paper of S. Hartman, Sur une condition supplémentaire dans les approximations Diophantiques tells you how to construct those from two consecutive convergents, and it is clear from the construction that those convergents are still, up to a power, "best approximations", which is what is needed here. For example, we have
$$n^{-49} \leq 1-b_n \leq n^{-1/7 + \epsilon}$$
for $n$ large enough, and if the irrationality measure of $\pi$ is $2$, then the exponent on the left can be replaced by $-1-\epsilon$ and on the right by $-1+\epsilon$.
Proofs.
Denote by $\Vert x \Vert$ the distance of $x$ to the nearest integer. We have that $\sin(k)$ is small when $k$ is close to a multiple of $\pi$, in which case $|\sin(k)| \asymp \Vert k/\pi \Vert$ by Taylor expansion. That is,
$$\begin{align*}
a_n &\asymp \inf_{1 \leq k \leq n, q \geq 1} \left \vert q\pi - k \right\vert \\
&\asymp \inf_{k \geq 1, 1 \leq q \leq \frac{n+1}\pi} \left \vert q\pi - k \right\vert
\end{align*} \,.$$
Define
$$a_n' = \inf_{k \geq 1, 1 \leq q \leq n} \left \vert q\pi - k \right\vert$$
(This is easier to work with, because Diophantine approximation applies more directly to estimating $a_n'$ rather than $a_n$.)
Let $\mu$ be the irrationality measure of $\pi$. If $(q_n)$ is the sequence of denominators of the continued fraction expansion of $\pi$, then $\mu = 1 + \limsup_{n \to \infty} \frac{\log q_{n+1}}{ \log q_n}$. (We have $2 \leq \mu \leq 7.6063$ and this recent preprint claims $\mu = 2$, but I haven't read that paper so I refer to Recent progress in the irrationality measure of $\pi$, https://mathoverflow.net/questions/178811/lower-bound-on-the-irrationality-measure-of-pi/178818#178818)
Because best approximations are convergents (see ProofWiki),
$$a_{q_n}' = \Vert q_n \pi \Vert$$
for all $n \geq 2$. For the same reason,
$$q_n^{-\mu - \epsilon + 1} \ll_\epsilon \Vert q_n \pi\Vert \ll_\epsilon q_n^{-\mu + \epsilon + 1}$$
Given $\epsilon > 0$ and $n$ large enough, we may find $m > 0$ with $n^{1/(\mu-1) - \epsilon} \leq q_m \leq n \leq q_{m+1} \leq n^{\mu-1+\epsilon}$. We then have
$$a_{q_{m+1}}' \leq a_n' \leq a_{q_m}' \,. $$
Taking $\log$'s and dividing by $\log n$:
$$(1-\mu + o(1)) \frac{\log q_{m+1}}{\log n} \leq \frac{\log a_n'}{\log n} \leq (1-\mu + o(1)) \frac{\log q_{m}}{\log n} \,.$$
Plugging in the bounds for $q_m, q_{m+1}$:
$$-(\mu-1)^2 + o(1) \leq \frac{\log a_n'}{\log n} \leq -1 + o(1) \,.$$
That is,
$$n^{-(\mu-1)^2 - \epsilon} \ll_\epsilon a_n' \ll_\epsilon n^{-1 + \epsilon} $$
and at this point we may replace $a_n'$ by $a_n$. To get explicit bounds, use that $\mu < 8$ to get
$$n^{-49} \leq a_n \ll_\epsilon n^{-1 + \epsilon} \,.$$

For $b_n = \sup_{1 \leq k \leq n} |\sin(k)|$: Similar manipulations lead to
$$\begin{align*}
1-b_n &\asymp \inf_{1 \leq k \leq n, q \geq 1 \; \text{odd}} \left \vert q\pi - 2k \right\vert \\
&\asymp \inf_{p \geq 1 \; \text{even}, 1 \leq q \leq \frac{2n+1}\pi \; \text{odd}} \left \vert q\pi - p \right\vert
\end{align*} \,.$$
Define
$$b_n' = \inf_{p \geq 1 \; \text{even}, 1 \leq q \leq n \; \text{odd}} \left \vert q\pi - p \right\vert \,.$$
The lower bound
$$n^{-(\mu-1)^2 - \epsilon} \ll_\epsilon b_n'$$
follows in the same way as before, by ignoring the condition that $p$ must be even and $q$ must be odd. For the upper bound, Hartman's construction gives you even $p$ and odd $q$ with $n^{1/(\mu-1) - \epsilon} \leq q \leq n$ and
$$|q \pi - p| \ll q^{-1+\epsilon}$$
(Here, the $q^{-1} = q^{-(\mu-1)/(\mu-1)}$ comes from the fact that the construction takes two convergents and takes appropriate linear combinations of the numerators and denominators. This causes the approximation to be worse by a power of $1/(\mu-1)$ relative to the size of the denominator.) This leads to
$$b_n' \ll_\epsilon n^{-1/(\mu-1) + \epsilon} \,.$$
