chudnovskySum — Mathlib

English

The infinite sum in Chudnovsky's formula for π⁻¹ is

Русский

Бесконечная сумма по формуле Чудновского для π⁻¹

LaTeX

$$$\\operatorname{chudnovskySum} = \\dfrac{12}{(640320)^{3/2}} \\sum_{n=0}^{\\infty} \\operatorname{chudnovskyTerm}(n).$$$

Lean4

/-- The infinite sum in Chudnovsky's formula for `π⁻¹` -/
noncomputable def chudnovskySum : ℝ :=
  12 / (640320 : ℝ) ^ (3 / 2 : ℝ) * ∑' n : ℕ, (chudnovskyTerm n : ℝ)

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