<s>[INST] Prove inequality $\arccos \left( \frac{\sin 1-\sin x}{1-x} \right) \leq \sqrt{\frac{1+x+x^2}{3}}$ I was trying to figure out if the following function can serve as a mean (see mean value theorem):
$$\arccos \left( \frac{\sin y-\sin x}{y-x} \right)$$
And turns out that for $x,y \leq \pi$ it does serve as a mean admirably.
But then I've noticed that for $0<x<1$ the following two functions are very close (see the picture):


Now how would you prove:
$$\arccos \left( \frac{\sin 1-\sin x}{1-x} \right) \leq \sqrt{\frac{1+x+x^2}{3}}$$

It's probably easier to consider another equivalent inequality:
$$\frac{\sin 1-\sin x}{1-x}  \geq \cos \sqrt{\frac{1+x+x^2}{3}}$$
Or even:
$$ \text{sinc} \left(\frac{1-x}{2} \right) \cos \left(\frac{1+x}{2} \right)  \geq \cos \sqrt{\frac{1+x+x^2}{3}}$$
We could use Taylor series, but that's too cumbersome in my opinion.
Another way would be Mean value theorem itself, but I encounter the same problem.

Is there a simple way to prove this inequality?

My calculus is not as sharp as it used to be (just kidding, it was never sharp).

Edit
Just to confirm (numerically) that the inequality holds, here is the plot of the difference between the two functions:

 [/INST] This is not a full answer, just a possible way to prove the inequality.
We use the following form of the inequality:
$$\text{sinc} \left(\frac{1-x}{2} \right) \cos \left(\frac{1+x}{2} \right)  \geq \cos \sqrt{\frac{1+x+x^2}{3}}$$
It makes sense to try infinite products, mainly because we get rid of the square root:
$$\text{sinc}(t)=\prod_{n=1}^\infty \left(1-\frac{t^2}{\pi^2 n^2} \right)$$
$$\cos (t)=\prod_{n=1}^\infty \left(1-\frac{t^2}{\pi^2 (n-1/2)^2} \right)$$
Thus, our inequality becomes:
$$\prod_{n=1}^\infty \left(1-\frac{(1-x)^2}{4\pi^2 n^2} \right) \left(1-\frac{(1+x)^2}{4\pi^2 (n-1/2)^2} \right) \geq \prod_{n=1}^\infty \left(1-\frac{1+x+x^2}{3\pi^2 (n-1/2)^2} \right)$$
Note that for $x<1$ every term in the infinite products is positive.
If, for example, every term of the product on the left is greater than every term of the product on the right, then our inequality is proven.
$$\left(1-\frac{(1-x)^2}{4\pi^2 n^2} \right) \left(1-\frac{(1+x)^2}{4\pi^2 (n-1/2)^2} \right) \geq^? 1-\frac{1+x+x^2}{3\pi^2 (n-1/2)^2}$$
After expanding and simplifying I obtained the following:
$$-\left(4 \pi^2 n(2n-3)+3(\pi^2-(1+x)^2) \right)(1-x)^2 \geq^? 0$$
And this is highly questionable, i.e. not correct for most cases. Remember, we are interested in the case $x < 1$, so:
$$4 \pi^2 n(2n-3)+3(\pi^2-(1+x)^2) \leq^? 0$$
$$4 \pi^2 n(2n-3)+3\pi^2 \leq^? 3 (1+x)^2$$
For $n=1$ we have a trivial inequality:
$$-\pi^2 < 3 (1+x)^2$$
But for $n \geq 2$ the inequality quickly stops working.
So this method probably doesn't prove anything.

On the other hand, we can compare the two term products on each side, i.e. prove that:
$$\prod_{n=k}^{k+1} \left(1-\frac{(1-x)^2}{4\pi^2 n^2} \right) \left(1-\frac{(1+x)^2}{4\pi^2 (n-1/2)^2} \right) \geq \prod_{n=k}^{k+1} \left(1-\frac{1+x+x^2}{3\pi^2 (n-1/2)^2} \right)$$
If that fails, we can try $3$ product terms and so on. This is just some algebra that a CAS can take care of even for a large number of terms.

Update
I decided to rearrange the second product so the terms are of the same order in $x$ and $n$:
$$\prod_{n=1}^\infty \left(1-\frac{1+x+x^2}{3\pi^2 (n-1/2)^2} \right)=\prod_{k=1}^\infty \left(1-\frac{1+x+x^2}{3\pi^2 (2k-3/2)^2} \right) \left(1-\frac{1+x+x^2}{3\pi^2 (2k-1/2)^2} \right)$$
Still, we have the same relation: only the first terms of the products obey the inequality, while all the rest seem to break it.
Below you can see the plot for:
$$ \dfrac{\left(1-\frac{(1-x)^2}{4\pi^2 n^2} \right) \left(1-\frac{(1+x)^2}{4\pi^2 (n-1/2)^2} \right) }{ \left(1-\frac{1+x+x^2}{3\pi^2 (2n-3/2)^2} \right) \left(1-\frac{1+x+x^2}{3\pi^2 (2n-1/2)^2} \right) }$$
For $x \in [0,1]$ and $n=1,2,3, \dots$.


I see no way to prove that the product of all terms for $n \geq 2$ is still closer to $1$ than the first term (despite numerical evidence), so this way doesn't seem to work as a proof of the original inequality.

</s>