noncomputable def ComplexLattice.nome (τ : UpperHalfPlane) : ℂ

The nome q = e^{2πiτ} associated to τ ∈ ℍ.

theorem ComplexLattice.g₂_qexpansion (τ : UpperHalfPlane) : PeriodPair.g₂ (ofUpperHalfPlane τ) = 4 * ↑Real.pi ^ 4 / 3 * (1 + 240 * ∑' (n : ℕ), ↑((ArithmeticFunction.sigma 3) (n + 1)) * nome τ ^ (n + 1))

Lemma 19.5 (q-expansion of g₂). For the lattice associated to τ ∈ ℍ, the Eisenstein-like coefficient g₂ of its Weierstrass form admits the q-expansion g₂(τ) = (4π⁴/3)·(1 + 240 ∑_{n≥1} σ₃(n) qⁿ), where σ₃(n) is the divisor sum ∑_{d|n} d³.

theorem ComplexLattice.g₃_qexpansion (τ : UpperHalfPlane) : PeriodPair.g₃ (ofUpperHalfPlane τ) = 8 * ↑Real.pi ^ 6 / 27 * (1 - 504 * ∑' (n : ℕ), ↑((ArithmeticFunction.sigma 5) (n + 1)) * nome τ ^ (n + 1))

Lemma 19.5 (q-expansion of g₃). For the lattice associated to τ ∈ ℍ, the coefficient g₃ admits the q-expansion g₃(τ) = (8π⁶/27)·(1 - 504 ∑_{n≥1} σ₅(n) qⁿ), where σ₅(n) = ∑_{d|n} d⁵.

theorem ComplexLattice.discriminant_product_formula (τ : UpperHalfPlane) : (ofUpperHalfPlane τ).discriminantLattice = (2 * ↑Real.pi) ^ 12 * nome τ * ∏' (n : ℕ), (1 - nome τ ^ (n + 1)) ^ 24

Lemma 19.5 (product formula for the modular discriminant). The discriminant Δ(τ) = g₂(τ)³ - 27 g₃(τ)² has the infinite-product q-expansion Δ(τ) = (2π)¹² · q · ∏_{n≥1} (1 - qⁿ)²⁴.