Documentation

Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Eisenstein Series #

Main definitions #

References #

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

The set of pairs of integers congruent to a mod N and with gcd equal to r.

Equations
Instances For
    theorem EisensteinSeries.gammaSet_one_const (r : ) (a a' : Fin 2ZMod 1) :
    gammaSet 1 r a = gammaSet 1 r a'

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

    theorem EisensteinSeries.gammaSet_one_eq (r : ) (a : Fin 2ZMod 1) :
    gammaSet 1 r a = {v : Fin 2 | (v 0).gcd (v 1) = r}

    For level N = 1, the gamma sets simplify to only a gcd condition.

    theorem EisensteinSeries.gammaSet_one_mem_iff (r : ) (v : Fin 2) :
    v gammaSet 1 r 0 (v 0).gcd (v 1) = r
    def EisensteinSeries.gammaSet_one_equiv (r : ) (a a' : Fin 2ZMod 1) :
    (gammaSet 1 r a) (gammaSet 1 r a')

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

    Equations
    Instances For
      @[reducible, inline]

      The map from Fin 2 → ℤ sending ![a,b] to a.gcd b.

      Equations
      Instances For
        theorem EisensteinSeries.finGcdMap_div {r : } [NeZero r] (v : Fin 2) (hv : finGcdMap v = r) :
        IsCoprime ((v / r) 0) ((v / r) 1)
        theorem EisensteinSeries.finGcdMap_smul {r : } (a : ) {v : Fin 2} (hv : finGcdMap v = r) :
        finGcdMap (a v) = a.natAbs * r
        @[reducible, inline]
        abbrev EisensteinSeries.divIntMap (r : ) {m : } (v : Fin m) :
        Fin m

        An abbreviation of the map which divides a integer vector by an integer.

        Equations
        Instances For
          theorem EisensteinSeries.mem_gammaSet_one (v : Fin 2) :
          v gammaSet 1 1 0 IsCoprime (v 0) (v 1)
          theorem EisensteinSeries.gammaSet_div_gcd {r : } {v : Fin 2} (hv : v gammaSet 1 r 0) (i : Fin 2) :
          r v i
          theorem EisensteinSeries.gammaSet_eq_gcd_mul_divIntMap {r : } {v : Fin 2} (hv : v gammaSet 1 r 0) :
          v = r divIntMap (↑r) v

          The equivalence between gammaSet 1 r 0 and gammaSet 1 1 0 for non-zero r.

          Equations
          Instances For

            The equivalence between (Fin 2 → ℤ) and Σ n : ℕ, gammaSet 1 n 0) .

            Equations
            Instances For
              theorem EisensteinSeries.vecMulSL_gcd {r : } [NeZero r] {v : Fin 2} (hab : finGcdMap v = r) (A : Matrix.SpecialLinearGroup (Fin 2) ) :

              Right-multiplying a vector by a matrix in SL(2, ℤ) doesn't change its gcd.

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