倭算数理研究所

科学・数学・学習関連の記事を、「倭マン日記」とは別に書いていくのだ!

spire (Scala) での円周率の計算 Machin (マチン)の公式

spire という Scala 用の数学ライブラリがあるんですが、そのコードで円周率の値を計算をするために Machin (マチン)の公式というのを使ってたので、その公式が正しいことを計算で確かめてみます。

Machin の公式は

  { \displaystyle
  \frac{\pi}{4} = 4 \arctan \frac{1}{5} - \arctan \frac{1}{239}
}

で与えられます。  { \arctan() } は逆正接関数で、これは与えられているとします。 ちょっとおどろおどろしい数値が入っていますが、証明はそこまで難しくありません。

準備

この公式の導出で使うのは正接の加法定理だけです。 正接の倍角の公式は加法定理からすぐ導けます:

  { \displaystyle
\begin{align*}
  \tan(x+y) &= \frac{\tan x + \tan y}{1 - \tan x \tan y} \\
  \tan 2\theta &= \frac{2\tan\theta}{1 - \tan^2\theta}
\end{align*}
}

導出は「三角関数の公式を復習する (3) : 三角関数の加法定理」などを参照。 そう言えば、 { \tan(-\theta) = - \tan\theta } も使うかな。

導出

 { \alpha = 4\arctan \frac{1}{5},\,\beta = \arctan \frac{1}{239} } とおくと、Machin の公式を示すには

  { \displaystyle
  \frac{\pi}{4} = \alpha - \beta
}

つまり

  { \displaystyle
  \tan(\alpha - \beta) = 1
}

を示せばいいことになります。

まず { \alpha } の定義より

  { \displaystyle
  \tan \frac{\alpha}{4} = \frac{1}{5}
}

なので、正接の倍角の公式より

  { \displaystyle
\begin{align*}
  \tan \frac{\alpha}{2}
    &= \frac{2\cdot\frac{1}{5}}{1-\left(\frac{1}{5}\right)^2} \\
    &= \frac{10}{24} \\
    &= \frac{5}{12}
\end{align*}
}

もう一度倍角の公式を使って

  { \displaystyle
\begin{align*}
  \tan \alpha
    &= \frac{2\cdot\frac{5}{12}}{1-\left(\frac{5}{12}\right)^2} \\
    &= \frac{2\cdot 5 \cdot 12}{12^2 - 5^2} \\
    &= \frac{120}{119} \\
    &= \frac{240}{238}
\end{align*}
}

最後の変形では、{ \beta } の中に 239 という数字があることを念頭に変形してます。

次に、{ \beta } の定義より

  { \displaystyle
  \tan \beta = \frac{1}{239}
}

さて、この結果を踏まえて { \tan(\alpha - \beta) } を計算すると

  { \displaystyle
\begin{align*}
  \tan(\alpha - \beta)
    &= \frac{\tan\alpha - \tan\beta}{1+\tan\alpha\tan\beta}  \\
    &= \frac{\frac{240}{238} - \frac{1}{239}}{1+\frac{240}{238}\cdot\frac{1}{239}} \\
    &= \frac{240\cdot 239 - 238}{238\cdot 239 + 240} \\
    &= \frac{(239+1)\cdot 239 - 238}{(239-1)\cdot 239 + 240} \\
    &= \frac{239^2 + 239 - 238}{239^2 -239 + 240} \\
    &= 1
\end{align*}
}

よって Machin の公式が示せました。 なんか、高校数学のちょうどよい演習問題って感じですな。

Javaによるアルゴリズム事典

Javaによるアルゴリズム事典