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 → ∞. See: https://en.wikipedia.org/wiki/Wallis_product

The proof can be broken down into two pieces. The first step (carried out in Mathlib/Analysis/SpecialFunctions/Integrals/Basic.lean) 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 π if 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 algebraic manipulation.

Main statements

• Real.Wallis.W: the product of the first k terms in Wallis' formula for π.
• Real.Wallis.W_eq_integral_sin_pow_div_integral_sin_pow: express W n as a ratio of integrals.
• Real.Wallis.W_le and Real.Wallis.le_W: upper and lower bounds for W n.
• Real.tendsto_prod_pi_div_two: the Wallis product formula.

noncomputable def Real.Wallis.W (k : ℕ) : ℝ

The product of the first k terms in Wallis' formula for π.

Equations

• Real.Wallis.W k = ∏ i ∈ Finset.range k, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3))

theorem Real.Wallis.W_succ (k : ℕ) : W (k + 1) = W k * ((2 * ↑k + 2) / (2 * ↑k + 1) * ((2 * ↑k + 2) / (2 * ↑k + 3)))

theorem Real.Wallis.W_pos (k : ℕ) : 0 < W k

theorem Real.Wallis.W_eq_factorial_ratio (n : ℕ) : W n = 2 ^ (4 * n) * ↑n.factorial ^ 4 / (↑(2 * n).factorial ^ 2 * (2 * ↑n + 1))

theorem Real.Wallis.W_eq_integral_sin_pow_div_integral_sin_pow (k : ℕ) : (Real.pi / 2)⁻¹ * W k = (∫ (x : ℝ) in 0..Real.pi, sin x ^ (2 * k + 1)) / ∫ (x : ℝ) in 0..Real.pi, sin x ^ (2 * k)

theorem Real.Wallis.W_le (k : ℕ) : W k ≤ Real.pi / 2

theorem Real.Wallis.le_W (k : ℕ) : (2 * ↑k + 1) / (2 * ↑k + 2) * (Real.pi / 2) ≤ W k

theorem Real.Wallis.tendsto_W_nhds_pi_div_two : Filter.Tendsto W Filter.atTop (nhds (Real.pi / 2))

theorem Real.tendsto_prod_pi_div_two : Filter.Tendsto (fun (k : ℕ) => ∏ i ∈ Finset.range k, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3))) Filter.atTop (nhds (Real.pi / 2))

Wallis' product formula for π / 2.