Wallis積分（高校数学）

1. $\sin^2x=\frac{1-\cos2x}2$ なので
   $$ \int_0^{\pi/2}\sin^2x\,dx=\Bigl[\frac x2-\frac{\sin2x}4\Bigr]_0^{\pi/2}=\frac\pi4-0=\frac\pi4 $$
   である。
2. $\sin^3x=\sin x(1-\cos^2x)$ であり、$(\cos x)'=-\sin x$ なので $\bigl(-\cos x+\frac{\cos^3x}3\bigr)'=\sin x-\cos^2x\sin x=\sin^3x$ である。よって
   $$ \int_0^{\pi/2}\sin^3x\,dx=\Bigl[-\cos x+\frac{\cos^3x}3\Bigr]_0^{\pi/2}=0-\Bigl(-1+\frac13\Bigr)=\frac23 $$
   である。

$\sin^0x=1$ なので $I_0=\int_0^{\pi/2}1\,dx=\frac\pi2$ である。また
$$ I_1=\int_0^{\pi/2}\sin x\,dx=\bigl[-\cos x\bigr]_0^{\pi/2}=-0-(-1)=1 $$
である。

$\cos^3t=\cos t(1-\sin^2t)$ であり、$\bigl(\sin t-\frac{\sin^3t}3\bigr)'=\cos t-\sin^2t\cos t=\cos^3t$ なので
$$ \int_0^{\pi/2}\cos^3t\,dt=\Bigl[\sin t-\frac{\sin^3t}3\Bigr]_0^{\pi/2}=1-\frac13=\frac23 $$
である。ex-wi-small の $I_3=\frac23$ と一致する。

ex-wi-first の $I_0=\frac\pi2$、$I_1=1$ から始めて thm-wi-recursion を使うと
$$ I_2=\frac12I_0=\frac\pi4,\qquad I_3=\frac23I_1=\frac23,\qquad I_4=\frac34I_2=\frac{3\pi}{16},\qquad I_5=\frac45I_3=\frac8{15}, $$
$$ I_6=\frac56I_4=\frac{5\pi}{32},\qquad I_7=\frac67I_5=\frac{16}{35} $$
である。$I_2=\frac\pi4$、$I_3=\frac23$ は ex-wi-small の高校の方法の答えと一致する。小数では $I_0,\dots,I_7$ は $1.5708,\ 1,\ 0.7854,\ 0.6667,\ 0.5890,\ 0.5333,\ 0.4909,\ 0.4571$ である（図 2）。

1. $m=2$：$\frac{4!}{4^2(2!)^2}=\frac{24}{16\cdot4}=\frac38$ なので $I_4=\frac38\cdot\frac\pi2=\frac{3\pi}{16}$ であり、ex-wi-table と一致する。
2. $m=3$：$\frac{4^3(3!)^2}{7!}=\frac{64\cdot36}{5040}=\frac{2304}{5040}=\frac{16}{35}$ なので $I_7=\frac{16}{35}$ であり、これも一致する。

• $n=2$：$2\,I_2I_1=2\cdot\frac\pi4\cdot1=\frac\pi2$。
• $n=3$：$3\,I_3I_2=3\cdot\frac23\cdot\frac\pi4=\frac\pi2$。
• $n=4$：$4\,I_4I_3=4\cdot\frac{3\pi}{16}\cdot\frac23=\frac\pi2$。
  $I_n$ に $\pi$ が入るのは偶数番目だけだが、隣どうしを掛けると、どの $n$ でも $\pi$ が 1 つだけ入る。

prop-wi-monotone から $I_{n}< I_{n-1}< I_{n-2}$ である。各辺を $I_{n-2}>0$ で割って thm-wi-recursion を使うと
$$ \frac{n-1}n<\frac{I_{n-1}}{I_{n-2}}<1 $$
となる。$n=10$ なら $0.9<\frac{I_9}{I_8}<1$ で、実際 $I_8=\frac{35\pi}{256}=0.4295\ldots$、$I_9=\frac{128}{315}=0.4063\ldots$ で、$\frac{I_9}{I_8}=0.9460\ldots$ である。$n$ が大きいと隣り合う 2 項はほとんど等しい。この評価を積の保存と組み合わせると、$I_n$ の大きさがおよそ $\sqrt{\frac\pi{2n}}$ だと分かる（Wallisの公式（高校数学））。

prf-thm-wi-recursion の段 2 は $n\ge2$ を使った。$n=1$ では、漸化式の右辺に現れる $I_{-1}=\int_0^{\pi/2}\frac{dx}{\sin x}$ が有限の値をもたないので、漸化式の右辺はそもそも意味をもたない（$0< x<\frac\pi2$ で $0<\sin x< x$ なので $\frac1{\sin x}>\frac1x$ であり、$0<\varepsilon<\frac\pi2$ について $\int_\varepsilon^{\pi/2}\frac{dx}{\sin x}>\int_\varepsilon^{\pi/2}\frac{dx}x=\log\frac{\pi}{2\varepsilon}$ は、$\varepsilon$ を $0$ に近づけると限りなく大きくなる）。
証明をたどると、何が崩れるかが分かる。$n=1$ では段 1 の境界の項は $\bigl[-\sin^0x\cos x\bigr]_0^{\pi/2}=\bigl[-\cos x\bigr]_0^{\pi/2}=1$ で、$0$ にならない。また、$n=1$ では $f(x)=\sin^0x=1$ は定数なので $f'(x)=0$ であり、残りの項 $\int_0^{\pi/2}f'(x)g(x)\,dx$ は $0$ である（段 1 の右辺の形 $(n-1)\int_0^{\pi/2}\sin^{n-2}x\cos^2x\,dx$ に $n=1$ を入れると、$0$ と有限の値をもたない積分 $\int_0^{\pi/2}\frac{\cos^2x}{\sin x}\,dx$ の積になり、値が定まらない。そこで、この形には代入しない）。よって段 1 の式は「$I_1=$（境界の項）$=1$」となるだけで、$I_1$ と $I_{-1}$ を結ぶ式は得られない。仮定 $n\ge2$ を外すと、漸化式は成り立たない。

prop-wi-cos は区間 $[0,\frac\pi2]$ で $\sin(\frac\pi2-t)=\cos t$ を使った。区間を $[0,\pi]$ にすると、
$$ \int_0^\pi\sin x\,dx=\bigl[-\cos x\bigr]_0^\pi=2,\qquad \int_0^\pi\cos x\,dx=\bigl[\sin x\bigr]_0^\pi=0 $$
で、値が違う。$x=\pi-t$ と置換すると $\sin$ は $\sin$ に移るが、$\cos$ には移らない。区間を替えると、少なくとも $n=1$ では「$\sin$ と $\cos$ の積分が等しい」という主張は崩れる（$n$ が偶数なら、$[0,\pi]$ でも $\int_0^\pi\sin^nx\,dx=\int_0^\pi\cos^nx\,dx$ である）。