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.pi, real.sin x ^ (2 * k + 1)) / ∫ (x : ℝ) in 0..real.pi, real.sin x ^ (2 * k)) filter.at_top (nhds 1)

source

theorem real.tendsto_prod_pi_div_two :

filter.tendsto (λ (k : ℕ), (finset.range k).prod (λ (i : ℕ), (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)))) filter.at_top (nhds (real.pi / 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.