W — Mathlib · SciLib

English

W(k) is the product of the first k Wallis factors, and is positive for all k.

Русский

W(k) — первый k множитель формулы Уоллиса, положителен для любого k.

LaTeX

$$W: \\mathbb{N} \\to \\mathbb{R},\\quad W(k) = \\prod_{i=0}^{k-1} \\frac{2i+2}{2i+1} \\cdot \\frac{2i+2}{2i+3}$$

Lean4

/-- The product of the first `k` terms in Wallis' formula for `π`. -/
noncomputable def W (k : ℕ) : ℝ :=
  ∏ i ∈ range k, (2 * i + 2) / (2 * i + 1) * ((2 * i + 2) / (2 * i + 3))

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