Documentation

TauCeti.NumberTheory.ModularForms.EisensteinSeries.QExpansion

The q-expansion of Eisenstein series with character #

For Dirichlet characters ψ modulo u and φ modulo v and a weight k ≥ 3 with ψ(-1) φ(-1) = (-1)^k, we compute the q-expansion of the Eisenstein series with character G_k^{ψ,φ}(z) = ∑_{(c, d) ∈ ℤ²} ψ(c) φ⁻¹(d) (c v z + d)^(-k) (TauCeti.EisensteinSeries.charEisensteinSeriesMF). Its constant coefficient is ψ(0) ∑_{d ∈ ℤ} φ⁻¹(d) d^(-k), and for n ≥ 1 its n-th coefficient is 2 (-2πi)^k / ((k-1)! v^k) ∑_{c m = n} ψ(c) φ̂(m) m^(k-1), where φ̂(m) = ∑_{r mod v} φ⁻¹(r) e^(2πi r m / v). When φ is primitive, φ̂(m) = g(φ⁻¹) φ(m) with g(φ⁻¹) the Gauss sum, so the n-th coefficient is a constant multiple of the twisted divisor sum σ_{k-1}^{ψ,φ}(n) = ∑_{d ∣ n} ψ(n/d) φ(d) d^(k-1).

The analytic input is a Lipschitz formula along residue classes: for any f : ZMod v → ℂ, ∑_{n ∈ ℤ} f(n) (z + n)^(-k) = (-2πi)^k / ((k-1)! v^k) ∑_{m ≥ 1} 𝓕f(-m) m^(k-1) e^(2πi m z / v), obtained by applying Mathlib's EisensteinSeries.qExpansion_identity_pnat to each residue class of n modulo v. The rows c and -c of G_k^{ψ,φ} contribute equally by the parity condition, the row c = 0 gives the constant term, and the remaining double series is regrouped by n = c m (HasSum.sum_divisorsAntidiagonal).

The coefficient-identification argument follows Mathlib's EisensteinSeries.E_qExpansion_coeff.

Main results #

References #

The Lipschitz formula along residue classes #

theorem TauCeti.EisensteinSeries.qExpansion_identity_zmod {v : ℕ} [NeZero v] (f : ZMod v → ℂ) {k : ℕ} (hk : 2 ≤ k) (z : UpperHalfPlane) :
∑' (n : ℤ), f ↑n * (↑z + ↑n) ^ (-↑k) = (-2 * ↑Real.pi * Complex.I) ^ k / (↑(k - 1).factorial * ↑v ^ k) * ∑' (m : ℕ+), ZMod.dft f (-↑↑m) * ↑↑m ^ (k - 1) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z / ↑v) ^ ↑m

The Lipschitz formula along residue classes. For a function f of residues modulo v, a weight k ≥ 2 and z in the upper half-plane, ∑_{n ∈ ℤ} f(n) (z + n)^(-k) = (-2πi)^k / ((k-1)! v^k) ∑_{m ≥ 1} 𝓕f(-m) m^(k-1) e^(2πi m z / v), where 𝓕f(-m) = ∑_{r mod v} f(r) e^(2πi r m / v) is the discrete Fourier transform of f. For v = 1 this is f 0 times Mathlib's EisensteinSeries.qExpansion_identity_pnat.

The Eisenstein series with character #

theorem TauCeti.EisensteinSeries.qExpansion_charEisensteinSeriesMF_coeff {u v N : ℕ} [NeZero v] [NeZero N] (ψ : DirichletCharacter ℂ u) (φ : DirichletCharacter ℂ v) {k : ℕ} (hk : 3 ≤ ↑k) (huv : u * v ∣ N) (hpar : ψ (-1) * φ (-1) = (-1) ^ k) (n : ℕ) :
(PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑(charEisensteinSeriesMF ψ φ hk huv)) = if n = 0 then ψ 0 * ∑' (d : ℤ), φ⁻¹ ↑d * ↑d ^ (-↑k) else 2 * (-2 * ↑Real.pi * Complex.I) ^ k / (↑(k - 1).factorial * ↑v ^ k) * ∑ x ∈ n.divisorsAntidiagonal, ψ ↑x.1 * ZMod.dft (⇑φ⁻¹) (-↑x.2) * ↑x.2 ^ (k - 1)

The q-expansion of the Eisenstein series with character. For characters ψ modulo u and φ modulo v with ψ(-1) φ(-1) = (-1)^k, the constant coefficient of G_k^{ψ,φ} is ψ(0) ∑_{d ∈ ℤ} φ⁻¹(d) d^(-k), and for n ≥ 1 its n-th coefficient is 2 (-2πi)^k / ((k-1)! v^k) ∑_{c m = n} ψ(c) φ̂(m) m^(k-1), where φ̂(m) = ∑_{r mod v} φ⁻¹(r) e^(2πi r m / v) is the discrete Fourier transform of φ⁻¹ at -m. (If the parity condition fails, the series is zero: charEisensteinSeriesMF_eq_zero.)

theorem TauCeti.EisensteinSeries.qExpansion_charEisensteinSeriesMF_coeff_of_isPrimitive {u v N : ℕ} [NeZero v] [NeZero N] (ψ : DirichletCharacter ℂ u) (φ : DirichletCharacter ℂ v) {k : ℕ} (hk : 3 ≤ ↑k) (huv : u * v ∣ N) (hpar : ψ (-1) * φ (-1) = (-1) ^ k) (hφ : φ.IsPrimitive) {n : ℕ} (hn : n ≠ 0) :

The q-expansion of the Eisenstein series with character, for primitive φ. Then the Fourier transform of φ⁻¹ is a multiple of φ by the Gauss sum g(φ⁻¹), and for n ≥ 1 the n-th coefficient of G_k^{ψ,φ} is 2 (-2πi)^k / ((k-1)! v^k) g(φ⁻¹) σ_{k-1}^{ψ,φ}(n), where σ_{k-1}^{ψ,φ}(n) = ∑_{d ∣ n} ψ(n/d) φ(d) d^(k-1) is the twisted divisor sum.