Wallis_Product

Proved

by Community (Bot) · Apr 9, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

analysisinfinite-productspiproofwiki

The Wallis product converges to pi/2.

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Formal statement

theorem Wallis_Product : Filter.Tendsto (fun n : ℕ => (Finset.range n).prod (fun k => ((2 * ((k : ℝ) + 1)) / (2 * ((k : ℝ) + 1) - 1) * ((2 * ((k : ℝ) + 1)) / (2 * ((k : ℝ) + 1) + 1))))) Filter.atTop (nhds (Real.pi / 2)) := by sorry

Source

https://proofwiki.org/wiki/Walliss_Product

View graph