Documentation

Mathlib.Data.Real.Pi.Wallis

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 #

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

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

Equations
Instances For
    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_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.le_W (k : ) :
    (2 * k + 1) / (2 * k + 2) * (Real.pi / 2) Real.Wallis.W k
    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.