How prove this inequality $\sin{\sin{\sin{\sin{x}}}}\le\frac{4}{5}\cos{\cos{\cos{\cos{x}}}}$

Nice Question:

let $x\in [0,2\pi]$, show that:

$$\sin{\sin{\sin{\sin{x}}}}\le\dfrac{4}{5}\cos{\cos{\cos{\cos{x}}}}?$$

I know this follow famous problem(1995 Russia Mathematical olympiad)

$$\sin{\sin{\sin{\sin{x}}}}<\cos{\cos{\cos{\cos{x}}}}$$

This problem solution can see :http://iask.games.sina.com.cn/b/19776980.html and everywhere have solution in china BBS

I post this problem solution

case1: if $x\in[\pi,2\pi]$,then $$\cos{\cos{\cos{\cos{x}}}}>0,\sin{\sin{\sin{\sin{x}}}}\le 0$$ so $$\cos{\cos{\cos{\cos{x}}}}>\sin{\sin{\sin{\sin{x}}}}$$

case2: if $x\in[0,\dfrac{\pi}{2}]$,then we have $$\cos{x}+\sin{x}\le\sqrt{2}<\dfrac{\pi}{2}\Longrightarrow 0\le \cos{x}<\dfrac{\pi}{2}-\sin{x}$$ so $$\cos{\cos{x}}>\cos{\left(\dfrac{\pi}{2}-\sin{x}\right)}=\sin{\sin{x}}$$ $$\sin{\cos{x}}<\sin{\left(\dfrac{\pi}{2}-\sin{x}\right)}=\cos{\sin{x}}$$ then $$\cos{\cos{\cos{x}}}<\cos{\sin{\sin{x}}}$$ so $$\cos{\cos{\cos{x}}}+\sin{\sin{\sin{x}}}<\cos{\sin{\sin{x}}}+\sin{\sin{\sin{x}}}<\dfrac{\pi}{2}$$ so $$\cos{\cos{\cos{x}}}<\dfrac{\pi}{2}-\sin{\sin{\sin{x}}}$$ then $$\cos{\cos{\cos{\cos{x}}}}>\cos{\left(\dfrac{\pi}{2}-\sin{\sin{\sin{x}}}\right)}=\sin{\sin{\sin{\sin{x}}}}$$ case3: if $x\in (\dfrac{\pi}{2},\pi)$,then let

$y=x-\dfrac{\pi}{2}$,so $$\cos{\cos{\cos{\sin{y}}}}>\sin{\sin{\cos{\sin{y}}}}$$ and since $f(t)=\sin{\sin{t}}$ is increasing,then $$f(\cos{\sin{y}})>f(\sin{\cos{y}})\Longrightarrow \sin{\sin{\cos{\sin{y}}}}>\sin{\sin{\sin{\cos{y}}}}$$ so $$\cos{\cos{\cos{\sin{y}}}}>\sin{\sin{\sin{\cos{y}}}}$$ so $$\cos{\cos{\cos{\cos{x}}}}>\sin{\sin{\sin{\sin{x}}}}$$

But I found this $\dfrac{4}{5}$ maybe is strong,

so if $x\in[\pi,2\pi]$,then we have $$\dfrac{4}{5}\cos{\cos{\cos{\cos{x}}}}\ge 0>\sin{\sin{\sin{\sin{x}}}}$$

But for the case $x\in [0,\pi]$, I can't prove this $$4\cos{\cos{\cos{\cos{x}}}}\ge 5\sin{\sin{\sin{\sin{x}}}}$$

Thank you very much！

We still start from the original Russian Olympiad Problem: $\cos \cos \cos \cos x> \sin \sin \sin \sin x$. It could have another numerical proof simply by doing in a calculator:

We have $-1\leq \cos x \leq 1, \text{that is }\cos 1\leq \cos \cos x\leq 1, \text{that is }\cos 1 \leq \cos \cos \cos x \leq \cos \cos 1$.

Finally, we have,

$$ ~0.6542 \simeq \cos \cos \cos 1\leq \cos \cos \cos \cos x \leq \cos \cos 1. $$

Similarly, we have

$$ -\sin \sin \sin \sin 1 \leq \sin \sin \sin \sin x \leq \sin \sin \sin 1 \simeq0.6784... $$

If the equation has the solution, that is

$$ \sin x\geq \sin^{-1} \sin^{-1}\sin ^{-1} \cos \cos \cos 1 \simeq 0.6086... $$

Thus, we have $$ |\cos x|\leq 0.7835... $$

Therefore, $\cos \cos \geq 0.7013 \to \cos \cos \cos x \leq 0.7639 \to \cos \cos \cos \cos \cos x \geq 0.7221...$

Thus, it is not possible to have $\sin \sin \sin \sin \sin \leq 0.6784.$ The inequality holds.

So, the $\frac{4}{5}$ is still not a strong constant, and inequality proof as similar.

Incomplete, but too long for a comment:

$\displaystyle f(x)\leqslant a\cdot g(x)\iff h(x)=\frac{f(x)}{g(x)}\leqslant a\iff$ We have to compute all solutions to $h'(x)=0$ , calculate the value of $h(x)$ in those points, as well as in $0$ and $2\pi$, which are the extremities of the interval, and verify $h(x_{_\text{k}})\leqslant a$, for all these $x_{_\text{k}}$ . Due to the function's parity and periodicity (cosine at the denominator, and an even number of sines in the numerator), the interval may just as well be restricted to $\Big[0,\frac\pi2\Big]$, since it can quite easily be shown that $h(x)=h(\pi-x)=-h(\pi+x)=$ $=h(2\pi+x)$. Either way, all its extrema are of the form $h(k\pi\pm x_0)$ and $h\left((2k+1)\frac\pi2\right)$, where $x_0\simeq1.1631454$ is the only solution to the transcendental equation $h'(x)=0$ on the open interval $\left(0,\frac\pi2\right)$. Indeed, $h\left((2k+1)\frac\pi2\right)\simeq0.791<h(k\pi\pm x_0)\simeq0.795<\displaystyle\frac45$. Now, that $h'(x)$ has roots in odd multiples of $\frac\pi2$ is trivial to show, but proving the uniqueness of $x_0$ on $\left(0,\frac\pi2\right)$ is anything but.