The Wallis Product for Pi #
This theorem establishes the Wallis Product for
π. Our proof is largely about analyzing
the behavior of the ratio of the integral of
sin x ^ n as
n → ∞.
The proof can be broken down into two pieces.
(Pieces involving general properties of the integral of
sin x ^n can be found
analysis.special_functions.integrals.) First, we use integration by parts to obtain a
recursive formula for
∫ x in 0..π, sin x ^ (n + 2) in terms of
∫ x in 0..π, sin x ^ n.
From this we can obtain closed form products of
∫ x in 0..π, sin x ^ (2 * n) and
∫ x in 0..π, sin x ^ (2 * n + 1) via induction. Next, we study the behavior of the ratio
∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)) / ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) and prove that
it converges to one using the squeeze theorem. The final product for
π is obtained after some