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
Instances For

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

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

    Equations
    Instances For

      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.
      Instances For

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

        Equations
        Instances For

          How the eisSummand function changes under the Moebius action.

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

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

          Equations
          Instances For

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

            Equations
            Instances For