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 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 π 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 = Finset.prod (Finset.range k) fun (i : ℕ) => (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3))

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

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

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

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

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

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

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

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

Wallis' product formula for π / 2.