Basic definitions for the Chudnovsky formula project

Shared definitions for the formalization of Milla's proof of the Chudnovsky formula (arXiv:1809.00533v6), targeting Mathlib's proof_wanted chudnovskySum_eq_pi_inv.

We define, on top of Mathlib's UpperHalfPlane, PeriodPair, E₄, E₆ and E2:

• Chudnovsky.Lτ : the period pair (1, τ) for τ : ℍ, giving the lattice ℤ + ℤτ;
• Chudnovsky.q : the nome q = exp (2πiτ) (Mathlib's Periodic.qParam 1);
• Chudnovsky.J : Klein's J-invariant E₄³ / (E₄³ - E₆²);
• Chudnovsky.E₂star : the non-holomorphic Eisenstein series E₂*(τ) = E₂(τ) - 3/(π Im τ);
• Chudnovsky.s₂ : Ramanujan's function s₂ = (E₄/E₆)·E₂*;
• Chudnovsky.τ₁₆₃, Chudnovsky.τ₈ : the CM points (1+i√163)/2 and i√2.

Following the plan in PLAN.md, J is defined directly in terms of Eisenstein series; the lattice-theoretic description g₂³/Δ becomes a lemma (proved in Fourier.lean).

def Chudnovsky.Lτ (τ : UpperHalfPlane) : PeriodPair

The period pair (1, τ) generating the lattice L_τ = ℤ + ℤτ for τ in the upper half-plane.

Equations

• Chudnovsky.Lτ τ = { ω₁ := 1, ω₂ := ↑τ, indep := ⋯ }

@[simp]

theorem Chudnovsky.Lτ_ω₁ (τ : UpperHalfPlane) : (Lτ τ).ω₁ = 1

@[simp]

theorem Chudnovsky.Lτ_ω₂ (τ : UpperHalfPlane) : (Lτ τ).ω₂ = ↑τ

noncomputable def Chudnovsky.q (τ : UpperHalfPlane) : ℂ

The nome q = exp (2πiτ), as Mathlib's Periodic.qParam with period 1.

Equations

• Chudnovsky.q τ = Function.Periodic.qParam 1 ↑τ

theorem Chudnovsky.q_eq (τ : UpperHalfPlane) : q τ = Complex.exp (2 * ↑Real.pi * Complex.I * ↑τ)

theorem Chudnovsky.norm_q (τ : UpperHalfPlane) : ‖q τ‖ = Real.exp (-(2 * Real.pi * τ.im))

theorem Chudnovsky.norm_q_lt_one (τ : UpperHalfPlane) : ‖q τ‖ < 1

noncomputable def Chudnovsky.J (τ : UpperHalfPlane) : ℂ

Klein's J-invariant, defined via Eisenstein series: J = E₄³ / (E₄³ - E₆²). The classical lattice description J = g₂³ / Δ is proved in Fourier.lean.

Equations

• Chudnovsky.J τ = ModularForm.E₄ τ ^ 3 / (ModularForm.E₄ τ ^ 3 - ModularForm.E₆ τ ^ 2)

theorem Chudnovsky.E₄_cube_sub_E₆_sq_ne_zero (τ : UpperHalfPlane) : ModularForm.E₄ τ ^ 3 - ModularForm.E₆ τ ^ 2 ≠ 0

The denominator of J never vanishes: E₄³ - E₆² = 1728·Δ and Δ ≠ 0.

theorem Chudnovsky.E₄_cube_sub_E₆_sq_eq_discriminant (τ : UpperHalfPlane) : ModularForm.E₄ τ ^ 3 - ModularForm.E₆ τ ^ 2 = 1728 * ModularForm.discriminant τ

theorem Chudnovsky.mul_J_eq (τ : UpperHalfPlane) : 1728 * J τ = ModularForm.E₄ τ ^ 3 / ModularForm.discriminant τ

1728·J = E₄³/Δ.

noncomputable def Chudnovsky.E₂star (τ : UpperHalfPlane) : ℂ

The non-holomorphic (quasi-modular) Eisenstein series E₂*(τ) = E₂(τ) - 3 / (π · Im τ).

Equations

• Chudnovsky.E₂star τ = EisensteinSeries.E2 τ - 3 / (↑Real.pi * ↑τ.im)

noncomputable def Chudnovsky.s₂ (τ : UpperHalfPlane) : ℂ

Ramanujan's function s₂(τ) = (E₄(τ)/E₆(τ)) · E₂*(τ).

Equations

• Chudnovsky.s₂ τ = ModularForm.E₄ τ / ModularForm.E₆ τ * Chudnovsky.E₂star τ

noncomputable def Chudnovsky.τ₁₆₃ : UpperHalfPlane

The CM point τ₁₆₃ = (1 + i√163)/2 of discriminant -163.

Equations

• Chudnovsky.τ₁₆₃ = { coe := { re := 1 / 2, im := √163 / 2 }, coe_im_pos := Chudnovsky.τ₁₆₃._proof_3 }

theorem Chudnovsky.τ₁₆₃_re : (↑τ₁₆₃).re = 1 / 2

@[simp]

theorem Chudnovsky.τ₁₆₃_im : τ₁₆₃.im = √163 / 2

noncomputable def Chudnovsky.τ₈ : UpperHalfPlane

The CM point τ₈ = i√2 of discriminant -8, used for the branch-of-square-root argument in the Main Theorem.

Equations

• Chudnovsky.τ₈ = { coe := { re := 0, im := √2 }, coe_im_pos := Chudnovsky.τ₈._proof_1 }

theorem Chudnovsky.τ₈_re : (↑τ₈).re = 0

@[simp]

theorem Chudnovsky.τ₈_im : τ₈.im = √2

def Chudnovsky.Region : Set UpperHalfPlane

All estimates in the paper hold on the region Im τ > 1.25.

Equations

• Chudnovsky.Region = {τ : UpperHalfPlane | 5 / 4 < τ.im}

theorem Chudnovsky.τ₁₆₃_mem_Region : τ₁₆₃ ∈ Region

theorem Chudnovsky.τ₈_mem_Region : τ₈ ∈ Region