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.

Equations

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

noncomputable def ModularForm.E {k : ℕ} (hk : 3 ≤ k) : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑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.eisensteinSeriesMF ⋯ 0).copy ⇑((1 / 2) • ModularForm.eisensteinSeriesMF ⋯ 0) ⋯ ModularForm.E._proof_7

@[reducible, inline]

noncomputable abbrev ModularForm.E₄ : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 4

The normalised level 1 Eisenstein series of weight 4.

Equations

• ModularForm.E₄ = ModularForm.E ModularForm.E₄._proof_1

@[reducible, inline]

noncomputable abbrev ModularForm.E₆ : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 6

The normalised level 1 Eisenstein series of weight 6.

Equations

• ModularForm.E₆ = ModularForm.E ModularForm.E₆._proof_1