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.

def ModularForm.eisensteinSeries_MF {k : ℤ} {N : ℕ+} (hk : 3 ≤ k) (a : Fin 2 → ZMod ↑N) : ModularForm (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.

Equations

• ModularForm.eisensteinSeries_MF hk a = { toFun := ⇑(EisensteinSeries.eisensteinSeries_SIF a k), slash_action_eq' := ⋯, holo' := ⋯, bdd_at_infty' := ⋯ }