The Wallis formula for Pi #
This file establishes the Wallis product for
real.tendsto_prod_pi_div_two). Our proof is
largely about analyzing the behaviour of the sequence
∫ x in 0..π, sin x ^ n as
n → ∞.
The proof can be broken down into two pieces. The first step (carried out in
analysis.special_functions.integrals) is to use repeated integration by parts to obtain an
explicit formula for this integral, which is rational if
n is odd and a rational multiple of
n is even.
The second step, carried out here, is to estimate 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
Main statements #
real.wallis.W: the product of the first
kterms in Wallis' formula for
W nas a ratio of integrals.
real.wallis.le_W: upper and lower bounds for
real.tendsto_prod_pi_div_two: the Wallis product formula.