Eisenstein series are Modular Forms

We show that Eisenstein series of weight k and level Γ(N) with congruence condition a : Fin 2 → ZMod N are Modular Forms.

TODO

Add q-expansions and prove that they are not all identically zero.

noncomputable def ModularForm.eisensteinSeriesMF {k : ℤ} {N : ℕ} [NeZero N] (hk : 3 ≤ k) (a : Fin 2 → ZMod N) : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k

This defines Eisenstein series as modular forms of weight k, level Γ(N) and congruence condition given by a : Fin 2 → ZMod N.

@[deprecated ModularForm.eisensteinSeriesMF (since := "2026-02-10")]

def ModularForm.eisensteinSeries_MF {k : ℤ} {N : ℕ} [NeZero N] (hk : 3 ≤ k) (a : Fin 2 → ZMod N) : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k

Alias of ModularForm.eisensteinSeriesMF.

---

This defines Eisenstein series as modular forms of weight k, level Γ(N) and congruence condition given by a : Fin 2 → ZMod N.

noncomputable def ModularForm.E {k : ℕ} (hk : 3 ≤ k) : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) ↑k

Normalised Eisenstein series of level 1 and weight k, here they have been scaled by 1/2 since we sum over coprime pairs.