Real.tendsto_prod_pi_div_two

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

This theorem states Wallis' product formula for `π / 2`. Specifically, it asserts that as the limit tends towards infinity (`Filter.atTop`), the product of the sequence defined by `(2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3))` for each natural number `i` in the range from 0 to `k` (`Finset.range k`), approaches the value `π / 2` (`nhds (Real.pi / 2)`). Hence, this theorem demonstrates that the product of this specified sequence tends to `π / 2` as the number of terms in the product increases without bound. It is a formalization of the famous mathematical result known as the Wallis' product formula for π.

More concisely: The limit as `i` approaches infinity of the product of `(2 * (i + 1)) / (2 * (i + 1) + 1)` and `(2 * (i + 1)) / (2 * (i + 1) + 2)` for `i` in the natural numbers, equals `π/2`.