Documentation

Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic

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 2ZMod N) :

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

Equations
Instances For
    noncomputable def ModularForm.E {k : } (hk : 3 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
    Instances For