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.
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' := ⋯ }
Instances For
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