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 ((1 + √-163) / 2) = -640320^3, and the other magic constants coming from Eisenstein series.

References

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

def chudnovskyNum (n : ℕ) : ℤ

The numerator of the nth term in Chudnovsky's series

def chudnovskyDenom (n : ℕ) : ℕ

The denominator of the nth term in Chudnovsky's series

def chudnovskyTerm (n : ℕ) : ℚ

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

noncomputable def chudnovskySum : ℝ

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