tendsto_prod_pi_div_two — Mathlib

English

Consider the finite products P_k = ∏_{i=0}^{k-1} [((2i+2)/(2i+1)) · ((2i+2)/(2i+3))]. As k → ∞, P_k converges to π/2.

Русский

Рассмотрим конечные произведения P_k = ∏_{i=0}^{k-1} [((2i+2)/(2i+1)) · ((2i+2)/(2i+3))]. При стремлении k к бесконечности, P_k сходится к π/2.

LaTeX

$$$\displaystyle \lim_{k \to \infty} \prod_{i=0}^{k-1} \left(\frac{2i+2}{2i+1} \cdot \frac{2i+2}{2i+3}\right) = \frac{\pi}{2}$$$

Lean4

/-- Wallis' product formula for `π / 2`. -/
theorem tendsto_prod_pi_div_two :
    Tendsto (fun k => ∏ i ∈ range k, ((2 : ℝ) * i + 2) / (2 * i + 1) * ((2 * i + 2) / (2 * i + 3))) atTop (𝓝 (π / 2)) :=
  Real.Wallis.tendsto_W_nhds_pi_div_two

Похожие утверждения