Constant terms of Eisenstein series at the cusps

For a weight W : (Fin 2 → ZMod N) → ℂ and k ≥ 3, the weighted Eisenstein series G_W(z) = ∑_{x ∈ ℤ²} W(x mod N) (x₀ z + x₁)^(-k) tends at i∞ to the sum of its row x₀ = 0, ∑_{n ∈ ℤ} W(0, n) n^(-k): every other summand decays like (Im z)^(-k), and the series is dominated uniformly on the imaginary axis. Since slashing by γ ∈ SL₂(ℤ) changes W to a ↦ W(a γ⁻¹), the constant term of G_W at the cusp γ ∞ = a / c is the sum over the multiples of the row (-c, a) of γ⁻¹: ∑_{n ∈ ℤ} W(-n c, n a) n^(-k).

For the Eisenstein series with character G_k^{ψ,φ}, with ψ modulo u and φ modulo v, this sum factors: the constant term at a / c vanishes unless v ∣ c, and then equals ψ(-c / v) φ⁻¹(a) ∑_{n ∈ ℤ} ψ(n) φ⁻¹(n) n^(-k). These are the constant-term vectors whose span is compared with the image of the constant-term map on M_k(N, χ) in the cusp–Eisenstein decomposition M_k(N, χ) = S_k(N, χ) ⊕ E_k(N, χ).

Main results

• TauCeti.EisensteinSeries.tendsto_weightedEisensteinSeries_atImInfty: the limit of G_W at i∞.
• TauCeti.EisensteinSeries.valueAtInfty_weightedEisensteinSeries_slash: the value at i∞ of every SL₂(ℤ)-translate of G_W.
• TauCeti.EisensteinSeries.constantTermAt_weightedEisensteinSeriesMF: the constant term of G_W at every cusp.
• TauCeti.EisensteinSeries.constantTermAt_charEisensteinSeriesMF: the constant term of G_k^{ψ,φ} at every cusp.
• TauCeti.EisensteinSeries.constantTermAt_charEisensteinSeriesMFRaise: the constant term of G_k^{ψ,φ}(tz) at every cusp, with the scaling factor (gcd(c,t)/t)^k.

References

• F. Diamond and J. Shurman, A first course in modular forms, §4.2 and §4.5.

theorem TauCeti.EisensteinSeries.tendsto_eisSummand_ofComplex_I_mul {k : ℤ} (hk : 0 < k) (x : Fin 2 → ℤ) : Filter.Tendsto (fun (t : ℝ) => EisensteinSeries.eisSummand k x (↑UpperHalfPlane.ofComplex (Complex.I * ↑t))) Filter.atTop (nhds (if x 0 = 0 then ↑(x 1) ^ (-k) else 0))

On the imaginary axis, a summand (x₀ z + x₁)^(-k) with x₀ ≠ 0 tends to 0, and a summand with x₀ = 0 is the constant x₁^(-k).

theorem TauCeti.EisensteinSeries.tendsto_weightedEisensteinSeries_atImInfty {N : ℕ} (W : (Fin 2 → ZMod N) → ℂ) {k : ℤ} [NeZero N] (hk : 3 ≤ k) : Filter.Tendsto (weightedEisensteinSeries W k) UpperHalfPlane.atImInfty (nhds (∑' (n : ℤ), W (Int.cast ∘ ![0, n]) * ↑n ^ (-k)))

The limit at i∞ of a weighted Eisenstein series: for k ≥ 3, the series ∑_{x ∈ ℤ²} W(x) (x₀ z + x₁)^(-k) tends to ∑_{n ∈ ℤ} W(0, n) n^(-k).

theorem TauCeti.EisensteinSeries.valueAtInfty_weightedEisensteinSeries {N : ℕ} (W : (Fin 2 → ZMod N) → ℂ) {k : ℤ} [NeZero N] (hk : 3 ≤ k) : UpperHalfPlane.valueAtInfty (weightedEisensteinSeries W k) = ∑' (n : ℤ), W (Int.cast ∘ ![0, n]) * ↑n ^ (-k)

The value at i∞ of a weighted Eisenstein series is the sum of its row x₀ = 0.

theorem TauCeti.EisensteinSeries.valueAtInfty_weightedEisensteinSeries_slash {N : ℕ} (W : (Fin 2 → ZMod N) → ℂ) {k : ℤ} [NeZero N] (hk : 3 ≤ k) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : UpperHalfPlane.valueAtInfty (SlashAction.map k γ (weightedEisensteinSeries W k)) = ∑' (n : ℤ), W (Int.cast ∘ ![-(n * ↑γ 1 0), n * ↑γ 0 0]) * ↑n ^ (-k)

The value at i∞ of a translated weighted Eisenstein series. For γ = !![a, b; c, d] ∈ SL₂(ℤ), the value at i∞ of G_W ∣[k] γ is ∑_{n ∈ ℤ} W(-n c, n a) n^(-k): only the multiples of the row (-c, a) of γ⁻¹ contribute, the pairs whose linear form vanishes at the cusp a / c.

theorem TauCeti.EisensteinSeries.constantTermAt_weightedEisensteinSeriesMF {N : ℕ} (W : (Fin 2 → ZMod N) → ℂ) {k : ℤ} [NeZero N] (hk : 3 ≤ k) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : (ModularForm.constantTermAt γ) (weightedEisensteinSeriesMF W hk) = ∑' (n : ℤ), W (Int.cast ∘ ![-(n * ↑γ 1 0), n * ↑γ 0 0]) * ↑n ^ (-k)

The constant term of a weighted Eisenstein series at every cusp. At the cusp represented by γ = !![a, b; c, d] ∈ SL₂(ℤ), the constant term of G_W is ∑_{n ∈ ℤ} W(-n c, n a) n^(-k).

theorem TauCeti.EisensteinSeries.constantTermAt_charEisensteinSeriesMF {N : ℕ} {k : ℤ} [NeZero N] {u v : ℕ} (ψ : DirichletCharacter ℂ u) (φ : DirichletCharacter ℂ v) (hk : 3 ≤ k) (huv : u * v ∣ N) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : (ModularForm.constantTermAt γ) (charEisensteinSeriesMF ψ φ hk huv) = if ↑v ∣ ↑γ 1 0 then ψ ↑(-(↑γ 1 0 / ↑v)) * φ⁻¹ ↑(↑γ 0 0) * ∑' (n : ℤ), ψ ↑n * φ⁻¹ ↑n * ↑n ^ (-k) else 0

The constant term of the Eisenstein series with character at every cusp. For ψ modulo u, φ modulo v with u v ∣ N, and γ = !![a, b; c, d] ∈ SL₂(ℤ), the constant term of G_k^{ψ,φ} at the cusp a / c is ψ(-c / v) φ⁻¹(a) ∑_{n ∈ ℤ} ψ(n) φ⁻¹(n) n^(-k) if v ∣ c, and 0 otherwise.

theorem TauCeti.EisensteinSeries.constantTermAt_charEisensteinSeriesMFRaise {N : ℕ} {k : ℤ} [NeZero N] {u v : ℕ} (ψ : DirichletCharacter ℂ u) (φ : DirichletCharacter ℂ v) {t : ℕ} (hk : 3 ≤ k) (htuv : t * (u * v) ∣ N) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : (ModularForm.constantTermAt γ) (charEisensteinSeriesMFRaise ψ φ t hk htuv) = (↑((↑γ 1 0).gcd ↑t) / ↑t) ^ k * if ↑v ∣ ↑γ 1 0 / ↑((↑γ 1 0).gcd ↑t) then ψ ↑(-(↑γ 1 0 / ↑((↑γ 1 0).gcd ↑t) / ↑v)) * φ⁻¹ ↑(↑t * ↑γ 0 0 / ↑((↑γ 1 0).gcd ↑t)) * ∑' (n : ℤ), ψ ↑n * φ⁻¹ ↑n * ↑n ^ (-k) else 0

The constant term of a raised character Eisenstein series at every cusp. At the cusp a/c, put g = gcd(c,t). The constant term of G_k^{ψ,φ}(tz) is (g/t)^k times ψ(-c/(gv)) φ⁻¹(ta/g) ∑ₙ ψ(n) φ⁻¹(n) n^(-k) when v ∣ c/g, and is zero otherwise. No primitivity or parity hypothesis is needed. The integer divisions are exact in the nonvanishing branch.