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.SpecialFunctions.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