Summability of E2

We collect here lemmas about the summability of the Eisenstein series E2 that will be used to prove how it transforms under the slash action.

theorem EisensteinSeries.hasSum_e2Summand_symmetricIcc (z : UpperHalfPlane) : HasSum (fun (x : ℤ) => e2Summand x z) (2 * riemannZeta 2 - 8 * ↑Real.pi ^ 2 * ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma 1) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ↑n) (SummationFilter.symmetricIcc ℤ)

theorem EisensteinSeries.summable_e2Summand_symmetricIcc (z : UpperHalfPlane) : Summable (fun (x : ℤ) => e2Summand x z) (SummationFilter.symmetricIcc ℤ)

theorem EisensteinSeries.G2_eq_tsum_cexp (z : UpperHalfPlane) : G2 z = 2 * riemannZeta 2 - 8 * ↑Real.pi ^ 2 * ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma 1) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ↑n

theorem EisensteinSeries.tendsto_e2Summand_atTop_nhds_zero (z : UpperHalfPlane) : Filter.Tendsto (fun (x : ℤ) => e2Summand x z) Filter.atTop (nhds 0)

theorem EisensteinSeries.hasSum_e2Summand_symmetricIco (z : UpperHalfPlane) : HasSum (fun (x : ℤ) => e2Summand x z) (2 * riemannZeta 2 - 8 * ↑Real.pi ^ 2 * ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma 1) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ↑n) (SummationFilter.symmetricIco ℤ)

theorem EisensteinSeries.summable_e2Summand_symmetricIco (z : UpperHalfPlane) : Summable (fun (x : ℤ) => e2Summand x z) (SummationFilter.symmetricIco ℤ)

theorem EisensteinSeries.G2_eq_tsum_symmetricIco (z : UpperHalfPlane) : G2 z = ∑'[SummationFilter.symmetricIco ℤ] (m : ℤ), e2Summand m z