arccos(cos(x)/(1+2cos(x)))の定積分

追記

この記事を公開してすぐに，この記事で紹介した定積分の式は Coxeter's integralと呼ばれていることを教えていただきました．
当時10代だったCoxeter(コクセター群で有名な人)が，Mathematical Gazette という雑誌に証明を募る形で発表し( link )，それに対してあのハーディーが手紙で返答した，というエピソードがあるようです．

詳しくは NahinのInside Interesting Integrals や，Coxeter の Twelve Geometric Essays の序文を参考にしてください．

前置き

約20年ほど前，私が大学一年生の頃，京大では吉田塾合宿というイベントがありました．合宿形式で数学の講義を聞いたり演習問題を解いたり刺激的で大変よいイベントだったのですが，そこで配られた演習問題の最後の問題が以下の問題でした．

式はシンプルなのに全然証明できないということで参加者の間でもかなり話題になったのですが，当時この問題を解けた参加者はいませんでした．
全く歯が立たない問題だったので，この問題は個人的な一生の未解決問題になりそうだなと思っていました．

そして時は流れ，いつのまにか積分の等式証明を生業とするような分野が自分の専門になりました．ふとこの問題のことを思い出してみると，やれば出来そうだなという感じだったので，この問題に決着をつけることにしました．

以下に証明を書きます．淡々と計算を進めるだけの証明でそれはそれで悪くないですが，計算量が多くエレガントな方法ではありません．もっといい方法があるよって方はぜひ教えていただけると嬉しいです．

なお，この問題の出題者が誰なのかも分かっていません．おそらく当時のチューターや教員あたりが問題リストを作成したのだと思いますが，この問題がオリジナルなのかそれとも何か出典があるのかも不明です．この問題について何か情報をお持ちの方がいれば，ぜひ教えていただけると嬉しいです．

証明

証明すべき式は
$$ \int_{-\frac{\pi}{2}}^{\frac{\pi}{2}}\arcsin(\frac{\cos x}{1+2\cos x})dx=\frac{\pi^{2}}{12}$$
と同値である．
さらに$a=\tan(x/2)$とすると、
\begin{eqnarray} &&\int_{-\frac{\pi}{2}}^{\frac{\pi}{2}}\arcsin(\frac{\cos x}{1+2\cos x})dx \\ &&=\int_{-1}^{1}\arcsin(\frac{1-a^{2}}{3-a^{2}})\frac{2da}{a^{2}+1}\\ &&=2\int_{-1}^{1}\arcsin(\frac{1-a^{2}}{3-a^{2}})\Im(\frac{1}{a-i})da\end{eqnarray}

となる。よって、
$$\Im\left(\int_{-1}^{1}\arcsin(\frac{1-a^{2}}{3-a^{2}})\frac{1}{a-i}da\right)=\frac{\pi^{2}}{24}$$
となることを示せばよい。
ここで部分積分より
\begin{eqnarray} &&\int_{-1}^{1}\arcsin\left(\frac{1-a^{2}}{3-a^{2}}\right)\frac{da}{a-i}\\&&= \left[\arcsin\left(\frac{1-a^{2}}{3-a^{2}}\right)\cdot\log(1+ia)\right]_{-1}^{1}\\ &&-\int_{-1}^{1}\left(\frac{d}{da}\left(\frac{a^{2}-1}{a^{2}-3}\right)\right)\frac{1}{\sqrt{1-\left(\frac{a^{2}-1}{a^{2}-3}\right)^{2}}}\log(1+ai)da\\ &&=-\int_{-1}^{1}\left(\frac{1}{a+\sqrt{3}}+\frac{1}{a-\sqrt{3}}\right)\frac{1}{\sqrt{2-a^{2}}}\log(1+ia)da\end{eqnarray}

となり，さらに被積分関数の偶奇性に着目して
$$\int_{-1}^{1}\left(\frac{1}{a+\sqrt{3}}+\frac{1}{a-\sqrt{3}}\right)\frac{\Im(\log(1+ia))}{\sqrt{2-a^{2}}}da=2\int_{-1}^{1}\frac{\Im(\log(1+ia))}{(a+\sqrt{3})\sqrt{2-a^{2}}}da $$
が分かる．よって示すべき式は
$$\Im\left(\int_{-1}^{1}\frac{\log(1+ia)}{(a+\sqrt{3})\sqrt{2-a^{2}}}da\right)=-\frac{\pi^{2}}{48} $$となる．さらに根号を含まない式を得るために$ a=\frac{t^{2}+2t-1}{1+t^{2}}$と変数変換すると
\begin{eqnarray} &&\int_{-1}^{1}\frac{1}{(a+\sqrt{3})\sqrt{2-a^{2}}}\log(1+ia)da\\ &=&\int_{0}^{1}\frac{1+t^{2}}{1+2t-t^{2}}d\log\left(\frac{t^{2}(1+\sqrt{3})+2t-1+\sqrt{3}}{1+t^{2}}\right)\log(1+i\frac{t^{2}+2t-1}{1+t^{2}})\\ &=&i\int_{0}^{1}\left(\frac{1}{t+\frac{\sqrt{3}-1}{1-i}}-\frac{1}{t+\frac{\sqrt{3}-1}{1+i}}\right)\log(1+i\frac{t^{2}+2t-1}{1+t^{2}})dt\\ \end{eqnarray}
となる．よって示すべき式は
$$\Re\left(\int_{0}^{1}\left(\frac{1}{t+\frac{\sqrt{3}-1}{1-i}}-\frac{1}{t+\frac{\sqrt{3}-1}{1+i}}\right)\log\left(1+i\frac{t^{2}+2t-1}{1+t^{2}}\right)dt\right)=-\frac{\pi^{2}}{48} $$となる．ここで，$$\left(\frac{1}{t+\frac{\sqrt{3}-1}{1-i}}-\frac{1}{t+\frac{\sqrt{3}-1}{1+i}}\right) $$ は純虚数であり，更に$$ \Im\left(\log\left(1+i\frac{t^{2}+2t-1}{1+t^{2}}\right)\right) =\Im\left(-\frac{\pi i}{4}+\int_{0}^{t}\left(\frac{du}{u+\frac{1+\sqrt{3}}{1-i}}+\frac{du}{u+\frac{1-\sqrt{3}}{1-i}}\right)\right)$$となるので，
\begin{eqnarray} &&\Re\left(\int_{0}^{1}\left(\frac{1}{t+\frac{\sqrt{3}-1}{1-i}}-\frac{1}{t+\frac{\sqrt{3}-1}{1+i}}\right)\log\left(1+i\frac{t^{2}+2t-1}{1+t^{2}}\right)dt\right)\\ &=&\Re\left(\int_{0}^{1}\left(\frac{1}{t+\frac{\sqrt{3}-1}{1-i}}-\frac{1}{t+\frac{\sqrt{3}-1}{1+i}}\right)\left(-\frac{\pi i}{4}+\int_{0}^{t}\left(\frac{du}{u+\frac{1+\sqrt{3}}{1-i}}+\frac{du}{u+\frac{1-\sqrt{3}}{1-i}}\right)\right)dt\right)\\ &=&-\frac{\pi^{2}}{12}+\Re\left(\int_{0< u< t<1}\left(\frac{du}{u+\frac{1+\sqrt{3}}{1-i}}+\frac{du}{u+\frac{1-\sqrt{3}}{1-i}}\right)\left(\frac{dt}{t+\frac{\sqrt{3}-1}{1-i}}-\frac{dt}{t+\frac{\sqrt{3}-1}{1+i}}\right)\right). \end{eqnarray}
よって示すべき式は
$$ \Re\left(\int_{0< u< t<1}\left(\frac{du}{u+\frac{1+\sqrt{3}}{1-i}}+\frac{du}{u+\frac{1-\sqrt{3}}{1-i}}\right)\left(\frac{dt}{t+\frac{\sqrt{3}-1}{1-i}}-\frac{dt}{t+\frac{\sqrt{3}-1}{1+i}}\right)\right)=\frac{\pi^{2}}{16}$$
となる．ここで後々の計算を楽にするために，$0$と$1$を固定して$ z:=\frac{1-\sqrt{3}}{1+i}$を無限に送るようなメビウス変換$ \alpha(t)=\frac{(1-z)t}{t-z}$によって積分の変数変換を行う．すると，示すべき式は
$$ \Re\left(\int_{0< u< t<1}\left(\frac{du}{u-\frac{3+\sqrt{3}-i-\sqrt{3}i}{4}}-\frac{du}{u-\frac{1+\sqrt{3}+i-\sqrt{3}i}{4}}\right)\left(\frac{dt}{t-\frac{1-\sqrt{-3}}{2}}\right)\right)=\frac{\pi^{2}}{16}$$
となる．以下では2重対数関数$ \mathrm{Li}_{2}(z)$の等式に帰着させて証明を行う．（2重対数関数の基本的性質については文献 dilog を参照）．左辺に公式
$$ \int_{0< u< t<1}\frac{du}{u-a}\frac{dt}{t-b}=\log\left(\frac{a-1}{a}\right)\log\left(\frac{b-1}{b-a}\right)+\mathrm{Li}_{2}\left(\frac{a-1}{a-b}\right)-\mathrm{Li}_{2}\left(\frac{a}{a-b}\right)$$
を適応し，$ \Re(\mathrm{Li}_{2}\left(-i\right))=-\frac{\pi^{2}}{48}$にも注意すると，示すべき式は
$$\Re\left(\mathrm{Li}_{2}\left(\frac{1+\sqrt{3}-i-\sqrt{3}i}{2}\right)+\mathrm{Li}_{2}\left(\frac{1-\sqrt{3}-i+\sqrt{3}i}{2}\right)\right)=\frac{\pi^{2}}{48} $$
となる．ここで5項関係式
\begin{eqnarray} &&\mathrm{Li}_{2}(x)+\mathrm{Li}_{2}(y)+\mathrm{Li}_{2}\left(\frac{1-x}{1-xy}\right)+\mathrm{Li}_{2}(1-xy)+\mathrm{Li}_{2}\left(\frac{1-y}{1-xy}\right)\\ &=&\frac{\pi^{2}}{2}-\log(x)\log(1-x)-\log(y)\log(1-y)-\log\left(\frac{1-x}{1-xy}\right)\log\left(\frac{1-y}{1-xy}\right) \end{eqnarray}
を少し変形して得られる式
\begin{eqnarray} &&\mathrm{Li}_{2}(1-x)+\mathrm{Li}_{2}(1-y)-\mathrm{Li}_{2}(\frac{1-x}{1-xy})-\mathrm{Li}_{2}(\frac{1-y}{1-xy})\\ &=&\mathrm{Li}_{2}(1-xy)-\frac{\pi^{2}}{6}-\log\left(\frac{1-x}{1-xy}\right)\log\left(\frac{1-y}{1-xy}\right) \end{eqnarray}
に
$$(x,y)=\left(\frac{1-\sqrt{3}-i-\sqrt{3}i}{2},\frac{1-\sqrt{3}+i+\sqrt{3}i}{2}\right) $$
を代入して
\begin{eqnarray} &&\mathrm{Li}_{2}\left(\frac{1+\sqrt{3}+i+\sqrt{3}i}{2}\right)+\mathrm{Li}_{2}\left(\frac{1+\sqrt{3}-i-\sqrt{3}i}{2}\right)-\mathrm{Li}_{2}\left(\frac{-1-\sqrt{3}-i-\sqrt{3}i}{2}\right)-\mathrm{Li}_{2}\left(\frac{-1-\sqrt{3}+i+\sqrt{3}i}{2}\right)\\ &=&\mathrm{Li}_{2}(-1)-\frac{\pi^{2}}{6}+\frac{\log(2+\sqrt{3})^{2}}{4}+\frac{9\pi^{2}}{16}\\ &=&\frac{5\pi^{2}}{16}+\frac{\log(2+\sqrt{3})^{2}}{4}.\tag{1} \label{eq1} \end{eqnarray}

さらに
$$ -\mathrm{Li}_{2}(z)=\mathrm{Li}_{2}(\frac{1}{z})+\frac{\pi^{2}}{6}+\frac{1}{2}\log(-z)^{2}$$
より
\begin{eqnarray} &&-\mathrm{Li}_{2}\left(\frac{-1-\sqrt{3}-i-\sqrt{3}i}{2}\right)-\mathrm{Li}_{2}\left(\frac{-1-\sqrt{3}+i+\sqrt{3}i}{2}\right)\\ &=&\mathrm{Li}_{2}\left(\frac{1-\sqrt{3}-i+\sqrt{3}i}{2}\right)+\mathrm{Li}_{2}\left(\frac{1-\sqrt{3}+i-\sqrt{3}i}{2}\right)+\frac{\pi^{2}}{3}+\frac{\log(2+\sqrt{3})^{2}}{4}-\frac{\pi^{2}}{16}\\ &=&\mathrm{Li}_{2}\left(\frac{1-\sqrt{3}-i+\sqrt{3}i}{2}\right)+\mathrm{Li}_{2}\left(\frac{1-\sqrt{3}+i-\sqrt{3}i}{2}\right)+\frac{\log(2+\sqrt{3})^{2}}{4}+\frac{13\pi^{2}}{48}.\tag{2} \label{eq2} \end{eqnarray}
よって，\eqref{eq1} と \eqref{eq2} より
$$ \mathrm{Li}_{2}\left(\frac{1+\sqrt{3}+i+\sqrt{3}i}{2}\right)+\mathrm{Li}_{2}\left(\frac{1+\sqrt{3}-i-\sqrt{3}i}{2}\right)+\mathrm{Li}_{2}\left(\frac{1-\sqrt{3}-i+\sqrt{3}i}{2}\right)+\mathrm{Li}_{2}\left(\frac{1-\sqrt{3}+i-\sqrt{3}i}{2}\right)=\frac{2\pi^{2}}{48}.$$
よって，示したい式の証明が得られた．

似た式

最後に数値実験で見つかる似た式をリストアップしておきます．