Documentation

Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Eisenstein Series #

Main definitions #

References #

def EisensteinSeries.gammaSet (N : ) (a : Fin 2ZMod N) :
Set (Fin 2)

The set of pairs of coprime integers congruent to a mod N.

Equations
theorem EisensteinSeries.gammaSet_one_eq (a a' : Fin 2ZMod 1) :

For level N = 1, the gamma sets are all equal.

def EisensteinSeries.gammaSet_one_equiv (a a' : Fin 2ZMod 1) :
(gammaSet 1 a) (gammaSet 1 a')

For level N = 1, the gamma sets are all equivalent; this is the equivalence.

Equations

Right-multiplying by γ ∈ SL(2, ℤ) sends gammaSet N a to gammaSet N (a ᵥ* γ).

The bijection between GammaSets given by multiplying by an element of SL(2, ℤ).

Equations
  • One or more equations did not get rendered due to their size.

The function on (Fin 2 → ℤ) whose sum defines an Eisenstein series.

Equations
def eisensteinSeries {N : } (a : Fin 2ZMod N) (k : ) (z : UpperHalfPlane) :

An Eisenstein series of weight k and level Γ(N), with congruence condition a.

Equations

The SlashInvariantForm defined by an Eisenstein series of weight k : ℤ, level Γ(N), and congruence condition given by a : Fin 2 → ZMod N.

Equations