Chudnovsky's formula for π

This file defines the infinite sum in Chudnovsky's formula for computing π⁻¹. It does not (yet!) contain a proof; anyone is welcome to adopt this problem, but at present we are a long way off.

Main definitions

• chudnovskySum: The infinite sum in Chudnovsky's formula

Future work

• Use this formula to give approximations for π.
• Prove the sum equals π⁻¹, as stated using proof_wanted below.
• Show that each imaginary quadratic field of class number 1 (corresponding to Heegner numbers) gives a Ramanujan type formula, and that this is the formula coming from 163, with $$j(\frac{1+\sqrt{-163}}{2}) = -640320^3$$, and the other magic constants coming from Eisenstein series.

References

• Milla, A detailed proof of the Chudnovsky formula
• Chen and Glebov, On Chudnovsky--Ramanujan type formulae

def chudnovskyNum (n : ℕ) : ℤ

The numerator of the nth term in Chudnovsky's series

Equations

• chudnovskyNum n = (-1) ^ n * ↑(6 * n).factorial * (545140134 * ↑n + 13591409)

def chudnovskyDenom (n : ℕ) : ℕ

The denominator of the nth term in Chudnovsky's series

Equations

• chudnovskyDenom n = (3 * n).factorial * n.factorial ^ 3 * 640320 ^ (3 * n)

def chudnovskyTerm (n : ℕ) : ℚ

The term at index n in Chudnovsky's series for π⁻¹

Equations

• chudnovskyTerm n = ↑(chudnovskyNum n) / ↑(chudnovskyDenom n)

noncomputable def chudnovskySum : ℝ

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

Equations

• chudnovskySum = 12 / 640320 ^ (3 / 2) * ∑' (n : ℕ), ↑(chudnovskyTerm n)