Primitive residue-class Eisenstein series and the cusps of Γ(N)

Mathlib's eisensteinSeries sums over primitive integer pairs in a specified residue class modulo N. In weight k ≥ 3 these series span a complement of the cusp forms in M_k(Γ(N)) (Diamond–Shurman, Theorem 4.2.3): this is the cusp–Eisenstein decomposition at level Γ(N), isCompl_primitiveEisensteinSubspace_cuspFormSubmodule. The span has the generator introduction rule mem_primitiveEisensteinSubspace and the finite-sum characterization mem_primitiveEisensteinSubspace_iff.

Only the pairs (0, 1) and (0, -1) survive at infinity. Consequently the constant term of the series with residue a at the cusp represented by γ detects whether a is ± the bottom row of γ⁻¹, with the sign (-1)^k for its negative. Directness follows: every cuspidal element of the span is zero. For spanning, the constant term of a modular form f on Γ(N) at γ depends only on that bottom row modulo N (ModularForm.constantTermAt_eq_of_vecMul_inv_eq), so giving the series with residue a half the constant term of f at any γ with that bottom row removes every constant term of f, the factor 1/2 compensating for the two residues ±a that see each cusp.

Main results

• TauCeti.EisensteinSeries.constantTermAt_eisensteinSeriesMF: the constant term of each series at every cusp.
• TauCeti.EisensteinSeries.disjoint_primitiveEisensteinSubspace_cuspFormSubmodule: the span meets the cusp forms only in 0.
• TauCeti.EisensteinSeries.sup_primitiveEisensteinSubspace_cuspFormSubmodule_eq_top: the span and the cusp forms together span M_k(Γ(N)).
• TauCeti.EisensteinSeries.isCompl_primitiveEisensteinSubspace_cuspFormSubmodule: the cusp–Eisenstein decomposition M_k(Γ(N)) = E_k(Γ(N)) ⊕ S_k(Γ(N)).

References

• F. Diamond and J. Shurman, A First Course in Modular Forms, §4.2.

The convergence argument uses Chris Birkbeck's Mathlib Eisenstein-series summability and vertical-strip estimates, and the summand limit in EisensteinSeries.ConstantTerm.

@[simp]

theorem TauCeti.EisensteinSeries.coe_eisensteinSeriesMF {N : ℕ} {k : ℤ} [NeZero N] (hk : 3 ≤ k) (a : Fin 2 → ZMod N) : ⇑(ModularForm.eisensteinSeriesMF hk a) = eisensteinSeries a k

The underlying function of the bundled primitive residue-class Eisenstein series.

theorem TauCeti.EisensteinSeries.tendsto_eisensteinSeries_atImInfty {N : ℕ} {k : ℤ} [NeZero N] (hk : 3 ≤ k) (a : Fin 2 → ZMod N) : Filter.Tendsto (eisensteinSeries a k) UpperHalfPlane.atImInfty (nhds ((if a = ![0, 1] then 1 else 0) + if a = ![0, -1] then (-1) ^ k else 0))

At infinity, a primitive residue-class Eisenstein series has constant term 1 for the residue (0, 1) and (-1)^k for (0, -1), adding both if the residues coincide.

@[simp]

theorem TauCeti.EisensteinSeries.valueAtInfty_eisensteinSeries {N : ℕ} {k : ℤ} [NeZero N] (hk : 3 ≤ k) (a : Fin 2 → ZMod N) : UpperHalfPlane.valueAtInfty (eisensteinSeries a k) = (if a = ![0, 1] then 1 else 0) + if a = ![0, -1] then (-1) ^ k else 0

The value at infinity of a primitive residue-class Eisenstein series.

theorem TauCeti.EisensteinSeries.constantTermAt_eisensteinSeriesMF {N : ℕ} {k : ℤ} [NeZero N] (hk : 3 ≤ k) (a : Fin 2 → ZMod N) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : (ModularForm.constantTermAt γ) (ModularForm.eisensteinSeriesMF hk a) = (if Matrix.vecMul a ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ) = ![0, 1] then 1 else 0) + if Matrix.vecMul a ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ) = ![0, -1] then (-1) ^ k else 0

The constant term at an arbitrary cusp is determined by the residue of the bottom row of the inverse cusp representative.

@[simp]

theorem TauCeti.EisensteinSeries.eisensteinSeriesMF_neg {N : ℕ} {k : ℤ} [NeZero N] (hk : 3 ≤ k) (a : Fin 2 → ZMod N) : ModularForm.eisensteinSeriesMF hk (-a) = (-1) ^ k • ModularForm.eisensteinSeriesMF hk a

Negating the residue class multiplies the primitive Eisenstein series by (-1)^k.

@[simp]

theorem TauCeti.EisensteinSeries.eisensteinSeriesMF_eq_zero_of_isEmpty {N : ℕ} {k : ℤ} [NeZero N] (hk : 3 ≤ k) (a : Fin 2 → ZMod N) [IsEmpty ↑(EisensteinSeries.gammaSet N 1 a)] : ModularForm.eisensteinSeriesMF hk a = 0

A residue class with no primitive integral lift has zero Eisenstein series.

noncomputable def TauCeti.EisensteinSeries.primitiveEisensteinSubspace {k : ℤ} (N : ℕ) [NeZero N] (hk : 3 ≤ k) : Submodule ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k)

The span of Mathlib's primitive residue-class Eisenstein series of level Γ(N) and weight k ≥ 3.

theorem TauCeti.EisensteinSeries.primitiveEisensteinSubspace_def {N : ℕ} {k : ℤ} [NeZero N] (hk : 3 ≤ k) : primitiveEisensteinSubspace N hk = Submodule.span ℂ (Set.range (ModularForm.eisensteinSeriesMF hk))

The defining span of the primitive Eisenstein subspace.

theorem TauCeti.EisensteinSeries.mem_primitiveEisensteinSubspace {N : ℕ} {k : ℤ} [NeZero N] (hk : 3 ≤ k) (a : Fin 2 → ZMod N) : ModularForm.eisensteinSeriesMF hk a ∈ primitiveEisensteinSubspace N hk

Each primitive residue-class series belongs to the primitive Eisenstein span.

theorem TauCeti.EisensteinSeries.mem_primitiveEisensteinSubspace_iff {N : ℕ} {k : ℤ} [NeZero N] (hk : 3 ≤ k) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k) : f ∈ primitiveEisensteinSubspace N hk ↔ ∃ (c : (Fin 2 → ZMod N) → ℂ), ∑ a : Fin 2 → ZMod N, c a • ModularForm.eisensteinSeriesMF hk a = f

Membership in the primitive Eisenstein span is equivalent to a finite sum indexed by residue pairs modulo N.

theorem TauCeti.EisensteinSeries.primitiveEisensteinSubspace_le {N : ℕ} {k : ℤ} [NeZero N] (hk : 3 ≤ k) {V : Submodule ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k)} (hV : ∀ (a : Fin 2 → ZMod N), ModularForm.eisensteinSeriesMF hk a ∈ V) : primitiveEisensteinSubspace N hk ≤ V

A subspace containing every primitive residue-class Eisenstein series contains their span.

theorem TauCeti.EisensteinSeries.disjoint_primitiveEisensteinSubspace_cuspFormSubmodule {N : ℕ} {k : ℤ} [NeZero N] (hk : 3 ≤ k) : Disjoint (primitiveEisensteinSubspace N hk) (ModularForm.cuspFormSubmodule (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k)

The primitive Eisenstein span and the cusp-form submodule have zero intersection.

theorem TauCeti.EisensteinSeries.sup_primitiveEisensteinSubspace_cuspFormSubmodule_eq_top {N : ℕ} {k : ℤ} [NeZero N] (hk : 3 ≤ k) : primitiveEisensteinSubspace N hk ⊔ ModularForm.cuspFormSubmodule (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k = ⊤

In weight k ≥ 3, the primitive residue-class Eisenstein series and the cusp forms together span M_k(Γ(N)).

theorem TauCeti.EisensteinSeries.isCompl_primitiveEisensteinSubspace_cuspFormSubmodule {N : ℕ} {k : ℤ} [NeZero N] (hk : 3 ≤ k) : IsCompl (primitiveEisensteinSubspace N hk) (ModularForm.cuspFormSubmodule (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k)

The cusp–Eisenstein decomposition at level Γ(N) in weight k ≥ 3: the primitive residue-class Eisenstein series span a complement of the cusp forms in M_k(Γ(N)).