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 : ℕ} [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.

Equations

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

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.

Equations

• ModularForm.E hk = (1 / 2) • ModularForm.eisensteinSeries_MF ⋯ 0