# Huygens' final unproved inequality

The analytic statement of Proposition XX in Huygens' "Inventa" is: If $$x> 0$$, and less than $$\frac{\pi}{2}$$, then

$$x>\sin x +\frac{10(4\sin^2\frac{x}{2}-\sin^2 x)}{12\sin\frac{x}{2}+9\sin x+8\frac{(2\sin\frac{x}{2}-\sin x)^2}{12\sin\frac{x}{2}+9\sin x}}.$$

The Taylor expansion of the right hand side at $$x=0$$ is:

$${}=x-\frac{29}{604800}x^7-\frac{47}{10368000}x^9-O(x^{11}).$$

It remains without proof to this day, although the asymptotic expansion shows its probably true. There is a proof of a similar inequality with "$$27$$" in place of "$$8$$", but Huygens' original statement remains unproved. One can see the extraordinary accuracy from the Taylor series, the error being of order "$$x^7$$." As I have said in earlier posts, I am preparing a paper on Huygens' approximations to $$\pi$$ and a proof would fill a gap in the literature.

• Do you have a response to the answer below? Commented Jul 28 at 2:17
• @IosifPinelis..your proof is the first known proof of Huygens' final inequality. Huygens, himself, writes that he obtained it by a more detailed study of the barycenter of a circular segment, but he gave no more details. He just states it without proof. Shuh gave a proof, using the position of the barycenter, of the inequality with "27" as the constant instead of "8" as in the above inequality. There is no known barycenter proof of his original inequality. I had hoped to furnish one using the inequality on the barycenter which I proposed and you proved. But, no luck so far. Commented Jul 28 at 15:49

$$\newcommand\th x$$As in my previous answers 1 and 2 to your questions, use the substitution $$t=\tan\frac\th4,\quad \sin\frac\th2=\frac{2t}{1+t^2}, \quad \cos\frac\th2=\frac{1-t^2}{1+t^2}, \quad \sin\th=\frac{4t(1-t^2)}{(1+t^2)^2}, \quad \th=4\tan^{-1}t$$ in this case to rewrite the inequality in question as $$\begin{equation*} f(t):= \frac{t \left(41 t^6-11 t^4-285 t^2-225\right)}{\left(t^2+1\right)^2 \left(41 t^4-90 t^2+225\right)}+\tan ^{-1}(t)>0 \tag{10}\label{10} \end{equation*}$$ for all $$\begin{equation*} t\in(0,t_*],\quad t_*:=\tan\frac\pi8=\sqrt{2}-1. \end{equation*}$$ One has $$\begin{equation*} f'(t)= -\frac{32 t^6 \left(41 t^4-2490 t^2-2175\right)}{\left(t^2+1\right)^3 \left(41 t^4-90 t^2+225\right)^2}>0 \end{equation*}$$ for $$t\in(0,t_*)$$.
Also, $$f(0+)=0$$. So, \eqref{10} immediately follows.
Note that $$\begin{equation*} f(t)= \frac{3712t^7}{4725}+O(t^9). \end{equation*}$$ So, the (lower) rational approximation of $$\tan ^{-1}(t)$$ given by \eqref{10}) may seem impressive; however, it it far from the best of its kind. Indeed, using Padé approximation, we get $$\begin{equation*} g(t)= \frac{16384 t^{17}}{703956825}+O(t^{19}), \end{equation*}$$ where $$\begin{equation*} g(t):= \tan ^{-1}(t)-\frac{t \left(15159 t^6+147455 t^4+345345 t^2+225225\right)}{35 \left(35 t^8+1260 t^6+6930 t^4+12012 t^2+6435\right)}, \tag{20}\label{20} \end{equation*}$$ so that we have a much better rational approximation of $$\tan ^{-1}(t)$$ with the same degrees of the numerator and the denominator as in the rational expression in \eqref{10}.
Moreover, $$\begin{equation*} g'(t)= \frac{16384 t^{16}}{\left(t^2+1\right) \left(35 t^8+1260 t^6+6930 t^4+12012 t^2+6435\right)^2}>0 \end{equation*}$$ for real $$t>0$$. Also, $$g(0+)=0$$. So, $$g(t)>0$$ for all real $$t>0$$. That is, the rational expression in \eqref{20} is a lower rational approximation of $$\tan ^{-1}(t)$$.