Documentation

Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs

Eisenstein Series E2 #

We define the Eisenstein series E2 of weight 2 and level 1 as a limit of partial sums over non-symmetric intervals.

source
def EisensteinSeries.e2Summand (m : ℤ) (z : UpperHalfPlane) :
ℂ

This is an auxilary summand used to define the Eisenstein serires G2.

Equations
Instances For
    source
    theorem EisensteinSeries.e2Summand_summable (m : ℤ) (z : UpperHalfPlane) :
    Summable fun (n : ℤ) => eisSummand 2 ![m, n] z
    source
    @[simp]
    theorem EisensteinSeries.e2Summand_zero_eq_two_riemannZeta_two (z : UpperHalfPlane) :
    e2Summand 0 z = 2 * riemannZeta 2
    source
    theorem EisensteinSeries.e2Summand_even (z : UpperHalfPlane) :
    Function.Even fun (x : ℤ) => e2Summand x z
    source
    def EisensteinSeries.G2 :
    UpperHalfPlane → ℂ

    The Eisenstein series of weight 2 and level 1 defined as the conditional sum of m in [N,N] of e2Summand m. This sum over symmetric intervals is handy in showing it is Summable.

    Equations
    Instances For
      source
      def EisensteinSeries.E2 :
      UpperHalfPlane → ℂ

      The normalised Eisenstein series of weight 2 and level 1. Defined as (1 / 2 * ζ(2)) * G2 .

      Equations
      Instances For
        source
        def EisensteinSeries.D2 (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) :
        UpperHalfPlane → ℂ

        This function measures the defect in G2 being a modular form.

        Equations
        Instances For
          source
          @[simp]
          theorem EisensteinSeries.D2_one :
          D2 1 = 0
          source
          theorem EisensteinSeries.D2_mul (A B : Matrix.SpecialLinearGroup (Fin 2) ℤ) :
          D2 (A * B) = SlashAction.map 2 B (D2 A) + D2 B
          source
          theorem EisensteinSeries.D2_inv (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) :
          SlashAction.map 2 A⁻¹ (D2 A) = -D2 A⁻¹
          source
          theorem EisensteinSeries.D2_T :
          D2 ModularGroup.T = 0
          source
          theorem EisensteinSeries.D2_S (z : UpperHalfPlane) :
          D2 ModularGroup.S z = 2 * ↑Real.pi * Complex.I / ↑z