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.

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

This is an auxiliary summand used to define the Eisenstein series G2.

theorem EisensteinSeries.e2Summand_summable (m : ℤ) (z : UpperHalfPlane) : Summable fun (n : ℤ) => eisSummand 2 ![m, n] z

@[simp]

theorem EisensteinSeries.e2Summand_zero_eq_two_riemannZeta_two (z : UpperHalfPlane) : e2Summand 0 z = 2 * riemannZeta 2

theorem EisensteinSeries.e2Summand_even (z : UpperHalfPlane) : Function.Even fun (x : ℤ) => e2Summand x z

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

noncomputable def EisensteinSeries.E2 : UpperHalfPlane → ℂ

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

noncomputable def EisensteinSeries.D2 (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : UpperHalfPlane → ℂ

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

@[simp]

theorem EisensteinSeries.D2_one : D2 1 = 0

theorem EisensteinSeries.D2_mul (A B : Matrix.SpecialLinearGroup (Fin 2) ℤ) : D2 (A * B) = SlashAction.map 2 B (D2 A) + D2 B

theorem EisensteinSeries.D2_inv (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) : SlashAction.map 2 A⁻¹ (D2 A) = -D2 A⁻¹

theorem EisensteinSeries.D2_T : D2 ModularGroup.T = 0

theorem EisensteinSeries.D2_S (z : UpperHalfPlane) : D2 ModularGroup.S z = 2 * ↑Real.pi * Complex.I / ↑z