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 → ∞
.
See: https://en.wikipedia.org/wiki/Wallis_product
The proof can be broken down into two pieces.
(Pieces involving general properties of the integral of sin x ^n
can be found
in 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
algebraic manipulation.