data.real.pi.wallis - mathlib docs

The Wallis Product for Pi #

theorem real.integral_sin_pow_div_tendsto_one :

filter.tendsto (λ (k : ℕ), (∫ (x : ℝ) in 0..π, real.sin x ^ (2 * k + 1)) / ∫ (x : ℝ) in 0..π, real.sin x ^ 2 * k) filter.at_top (𝓝 1)

source

theorem real.tendsto_prod_pi_div_two :

filter.tendsto (λ (k : ℕ), ∏ (i : ℕ) in finset.range k, ((2 * ↑i + 2) / (2 * ↑i + 1)) * ((2 * ↑i + 2) / (2 * ↑i + 3))) filter.at_top (𝓝 (π / 2))

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.