Low-order q-expansion coefficients at level one

Mathlib records the constant and linear q-coefficients of E₄, E₆ and Δ. This file continues them to the q² and q³ terms, E₄ = 1 + 240 q + 2160 q² + 6720 q³ + ⋯, E₆ = 1 - 504 q - 16632 q² - 122976 q³ + ⋯ and Δ = q - 24 q² + 252 q³ + ⋯, and records that Δ is asymptotic to q at i∞. These are the coefficients the q-expansion of the modular invariant j = E₄³ / Δ is computed from.

The Eisenstein coefficients are 240 σ₃(n) and -504 σ₅(n) (Mathlib's EisensteinSeries.E_qExpansion_coeff). The coefficients of Δ are read off the identity 1728 Δ = E₄³ - E₆² in the graded ring, transported to q-expansions.

Main results

• TauCeti.ModularForm.qExpansion_discriminant_eq_E₄_cube_sub_E₆_sq: the q-expansion of Δ is (E₄³ - E₆²) / 1728, computed on power series.
• TauCeti.ModularForm.discriminant_qExpansion_coeff_two, TauCeti.ModularForm.discriminant_qExpansion_coeff_three: τ(2) = -24 and τ(3) = 252.
• TauCeti.ModularForm.tendsto_discriminant_div_qParam_atImInfty: Δ / q → 1 at i∞.

References

• J.-P. Serre, A Course in Arithmetic, VII.4 — the expansions of E₄, E₆ and Δ.

theorem TauCeti.ModularForm.E₄_qExpansion_coeff_two : (PowerSeries.coeff 2) (UpperHalfPlane.qExpansion 1 ⇑ModularForm.E₄) = 2160

The q²-coefficient of E₄ is 240 σ₃(2) = 2160.

theorem TauCeti.ModularForm.E₄_qExpansion_coeff_three : (PowerSeries.coeff 3) (UpperHalfPlane.qExpansion 1 ⇑ModularForm.E₄) = 6720

The q³-coefficient of E₄ is 240 σ₃(3) = 6720.

theorem TauCeti.ModularForm.E₆_qExpansion_coeff_two : (PowerSeries.coeff 2) (UpperHalfPlane.qExpansion 1 ⇑ModularForm.E₆) = -16632

The q²-coefficient of E₆ is -504 σ₅(2) = -16632.

theorem TauCeti.ModularForm.E₆_qExpansion_coeff_three : (PowerSeries.coeff 3) (UpperHalfPlane.qExpansion 1 ⇑ModularForm.E₆) = -122976

The q³-coefficient of E₆ is -504 σ₅(3) = -122976.

theorem TauCeti.ModularForm.qExpansion_discriminant_eq_E₄_cube_sub_E₆_sq : UpperHalfPlane.qExpansion 1 ModularForm.discriminant = 1728⁻¹ • (UpperHalfPlane.qExpansion 1 ⇑ModularForm.E₄ ^ 3 - UpperHalfPlane.qExpansion 1 ⇑ModularForm.E₆ ^ 2)

The q-expansion of the discriminant is (E₄³ - E₆²) / 1728, the image of Mathlib's ModularForm.discriminant_eq_E₄_cube_sub_E₆_sq_graded under the q-expansion algebra homomorphism ModularForm.qExpansionAlgHom.

theorem TauCeti.ModularForm.discriminant_qExpansion_coeff_zero : (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 ModularForm.discriminant) = 0

The constant coefficient of the discriminant vanishes: Δ is a cusp form.

theorem TauCeti.ModularForm.discriminant_qExpansion_coeff_two : (PowerSeries.coeff 2) (UpperHalfPlane.qExpansion 1 ModularForm.discriminant) = -24

The q²-coefficient of the discriminant is Ramanujan's τ(2) = -24.

theorem TauCeti.ModularForm.discriminant_qExpansion_coeff_three : (PowerSeries.coeff 3) (UpperHalfPlane.qExpansion 1 ModularForm.discriminant) = 252

The q³-coefficient of the discriminant is Ramanujan's τ(3) = 252.

theorem TauCeti.ModularForm.tendsto_discriminant_div_qParam_atImInfty : Filter.Tendsto (fun (τ : UpperHalfPlane) => ModularForm.discriminant τ / Function.Periodic.qParam 1 ↑τ) UpperHalfPlane.atImInfty (nhds 1)

The discriminant is asymptotic to q at i∞: Δ / q → 1.