The Wallis formula for Pi #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source

noncomputable def real.wallis.W (k : ℕ) :

ℝ

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

Equations

real.wallis.W k = (finset.range k).prod (λ (i : ℕ), (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)))

source

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)))

source

theorem real.wallis.W_pos (k : ℕ) :

0 < real.wallis.W k

source

theorem real.wallis.W_eq_factorial_ratio (n : ℕ) :

real.wallis.W n = 2 ^ (4 * n) * ↑(n.factorial) ^ 4 / (↑((2 * n).factorial) ^ 2 * (2 * ↑n + 1))

source

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)

source

theorem real.wallis.W_le (k : ℕ) :

real.wallis.W k ≤ real.pi / 2

source

theorem real.wallis.le_W (k : ℕ) :

(2 * ↑k + 1) / (2 * ↑k + 2) * (real.pi / 2) ≤ real.wallis.W k

source

theorem real.wallis.tendsto_W_nhds_pi_div_two :

filter.tendsto real.wallis.W filter.at_top (nhds (real.pi / 2))

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))

Wallis' product formula for π / 2.