# mathlib3documentation

data.real.pi.wallis

# 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.
noncomputable def real.wallis.W (k : ) :

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

Equations
theorem real.wallis.W_succ (k : ) :
real.wallis.W (k + 1) = * ((2 * k + 2) / (2 * k + 1) * ((2 * k + 2) / (2 * k + 3)))
theorem real.wallis.W_pos (k : ) :
theorem real.wallis.W_eq_factorial_ratio (n : ) :
= 2 ^ (4 * n) * (n.factorial) ^ 4 / (((2 * n).factorial) ^ 2 * (2 * n + 1))
theorem real.wallis.W_le (k : ) :
theorem real.wallis.le_W (k : ) :
(2 * k + 1) / (2 * k + 2) * (real.pi / 2)
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.