My question : Is it true that $|\cos(k)| \geq \frac{1}{2^k}$ for all integers $k\geq 0$ ?
What I tried : I have checked with a computer that the inequality holds for
$0 \leq k \leq 4\times 10^5$. I can also show that the set of $k$ for which the inequality holds is infinite ; in fact, it has density at least $\frac{1}{2}$.
To see that :
Lemma. For $x\in{\mathbb R}$, one has $(*):|\cos(x+1)|+|\cos(x+2)| \geq \frac{3}{4}$.
Corollary of lemma. For $x\in{\mathbb R}$, either $|\cos(x+1)|\geq \frac{|\cos(x)|}{2}$ or $|\cos(x+2)|\geq \frac{|\cos(x)|}{4}$.
Putting $x=k$ in the corollary, we then see that if the inequality holds
for $k$, it will also hold for $k+1$ or $k+2$.
Proof of lemma. Let $f_1(x)=|\cos(x+1)|$ and $f_2(x)=|\cos(x+2)|$. Since
$f_1$ and $f_2$ are $\pi$-periodic, it suffices to show $(*)$ on $[0,\pi]$. Now,
write $[0,\pi]=I_1 \cup I_2 \cup I_3$ where $I_1=[0,\frac{\pi}{2}-1]$, $I_2=[\frac{\pi}{2}-1,\frac{3\pi}{2}-2]$ and $I_3=[\frac{3\pi}{2}-2,\pi]$. Then
$f_1$ and $f_2$ are concave on each of the $I_j$, so it suffices to check (*) on the endpoints, and this is easy.
UPDATE 04/09/2019 : We can use the fact that $\pi$ has irrationality
measure at most $8$ (as explained in the accepted answer to this older question, thanks to i707107 for providing the link). Indeed (in all this section every inequality is meant to hold for all but finitely many $k$), denote by $a_k$ an integer such that $a_k\frac{\pi}{2}$ is closest possible to $k$, so that $$\Big|k-\frac{a_k\pi}{2}\Big| \leq \frac{\pi}{4}\tag{1}$$.
Then $\Big|\pi-\frac{2k}{a_k}\Big| \geq \frac{1}{a_k^8}$. Now $a_k \sim \frac{2k}{\pi}$, so $a_k \gt \frac{k}{\pi}$. It follows that $$\Big|\frac{a_k\pi}{2}-k\Big| \geq \frac{1}{2a_k^7} \geq \frac{\pi^8}{2^7k^7}\tag{2}$$.
There are then two cases :
If $a_k$ is even then $|\cos(k)|\geq Constant\geq \frac{1}{2^k}$. If, on the other hand, $a_k$ is odd, then then finite increments inequality yields $\Big|\frac{\cos(k)-\cos(\frac{a_k\pi}{2})}{k-\frac{a_k\pi}{2}}\Big| \geq Constant$ so that $|\cos(k)| \geq Constant \times |k-\frac{a_k\pi}{2}|$.
So my inequality holds for all except finitely many $k$.
Best Answer
I eventually found a proof, based on i707107's suggestion. By using a computer program with sufficient precision, one can check that the inequality holds for $k<316$. So it will suffice to show the inequality for $k\geq 316$.
Denote by $a_k\frac{\pi}{2}$ the integral multiple of $\frac{\pi}{2}$ that's closest to $k$, so that $\varepsilon_k=\big|k-a_k\frac{\pi}{2}\big| \leq \frac{\pi}{4}$. Then $k=a_k\frac{\pi}{2}\pm\varepsilon_k$.
If $a_k$ is even, then $\cos(a_k\frac{\pi}{2})=\pm 1$ and hence $|\cos(k)|=|\cos(\varepsilon_k)| \geq \frac{\sqrt{2}}{2}$ and we are done. So we may assume without loss that $a_k$ is odd.
Then $\cos(a_k\frac{\pi}{2})=0$. Using the finite increments formula, there is a $\xi \in [a_k\frac{\pi}{2}-\frac{\pi}{4},a_k\frac{\pi}{2}+\frac{\pi}{4}]$ such that $\frac{\cos(k)-\cos(a_k\frac{\pi}{2})}{k-a_k\frac{\pi}{2}}=-\sin(\xi)$. It follows that $\Big|\frac{\cos(k)-\cos(a_k\frac{\pi}{2})}{k-a_k\frac{\pi}{2}}\Big| \geq \frac{\sqrt{2}}{2}$, so that
$$ \begin{array}[lcl] \big|\cos(k)\big| &\geq& \frac{\sqrt{2}}{2} \Big|k-a_k\frac{\pi}{2}\Big| \\ &=& \frac{\sqrt{2}a_k}{4} \Big|\frac{2k}{a_k}-\pi\Big| \\ &\geq& \frac{\sqrt{2}a_k}{4} \frac{1}{a_k^{42}}=\frac{1}{\sqrt{8}a_k^{41}} \\ &\geq& \frac{1}{\sqrt{8}\big(\frac{2k}{\pi}+\frac{1}{2}\big)^{41}} \\ \end{array} $$
So, the inequality we want follows from
$$ 2^{k} \geq \sqrt{8}\bigg(\frac{2k}{\pi}+\frac{1}{2}\bigg)^{41} $$
which can be written as $f(k)\geq 0$ where $f(k)=2^{\frac{k-\frac{3}{2}}{41}}-\big(\frac{2k}{\pi}+\frac{1}{2}\big)$. We have $f'(x)=\frac{\ln(2)}{41}2^{\frac{k-\frac{3}{2}}{41}}-\frac{2}{\pi}$ so that $f'(x)\geq 0$ for $x\geq 3$. So for $k\geq 316$, we have $f(k)\geq f(316) \gt 0$ which finishes the proof.