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.

Main Results

The key results concern the difference between two different orders of summation for the telescoping series ∑_{m,n} (1/(mz + n) - 1/(mz + n + 1)):

1. tsum_symmetricIco_tsum_sub_eq: Summing first over n (in symmetric intervals), then m: ∑'[symmetricIco] n : ℤ, ∑' m : ℤ, (1/(mz+n) - 1/(mz+n+1)) = -2πi/z

2. tsum_tsum_symmetricIco_sub_eq: Summing first over m, then n (in symmetric intervals): ∑' m : ℤ, ∑'[symmetricIco] n : ℤ, (1/(mz+n) - 1/(mz+n+1)) = 0

The difference -2πi/z between these two orderings is precisely the correction term D2 that appears in the transformation formula for G2 under the action of S.

Proof Strategy

1. For fixed m ≠ 0, the inner sum over n telescopes to zero (each term cancels with its neighbor), establishing the first identity.

2. For fixed n, the inner sum over m can be computed using the cotangent series expansion. As n → ±∞ in symmetric intervals, these sums contribute -2πi/z.

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.E2_eq_tsum_cexp (z : UpperHalfPlane) : E2 z = 1 - 24 * ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma 1) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ↑n

The q-expansion of the normalised weight-2 Eisenstein series: E₂(z) = 1 - 24 ∑_{n≥1} σ₁(n) qⁿ.

theorem EisensteinSeries.hasSum_qExpansion_E2 (z : UpperHalfPlane) : HasSum (fun (m : ℕ) => (if m = 0 then 1 else -24 * ↑((ArithmeticFunction.sigma 1) m)) • Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ m) (E2 z)

The q-expansion of E2 as a HasSum over ℕ.

theorem EisensteinSeries.isBoundedAtImInfty_E2 : UpperHalfPlane.IsBoundedAtImInfty E2

E2 is bounded at i∞.

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

theorem EisensteinSeries.summable_left_one_div_linear_sub_one_div_linear (z : UpperHalfPlane) (a b : ℤ) : Summable fun (m : ℤ) => 1 / (↑m * ↑z + ↑a) - 1 / (↑m * ↑z + ↑b)

theorem EisensteinSeries.summable_right_one_div_linear_sub_one_div_linear_succ (z : UpperHalfPlane) (m : ℤ) : Summable fun (b : ℤ) => 1 / (↑m * ↑z + ↑b) - 1 / (↑m * ↑z + ↑b + 1)

theorem EisensteinSeries.tendsto_double_sum_S_act (z : UpperHalfPlane) : Filter.Tendsto (fun (N : ℕ) => ∑' (n : ℤ), ∑ m ∈ Finset.Ico (-↑N) ↑N, 1 / (↑n * ↑z + ↑m) ^ 2) Filter.atTop (nhds ((↑z ^ 2)⁻¹ * G2 (ModularGroup.S • z)))

theorem EisensteinSeries.tsum_symmetricIco_tsum_eq_S_act (z : UpperHalfPlane) : ∑'[SummationFilter.symmetricIco ℤ] (n : ℤ), ∑' (m : ℤ), 1 / (↑m * ↑z + ↑n) ^ 2 = (↑z ^ 2)⁻¹ * G2 (ModularGroup.S • z)

theorem EisensteinSeries.tsum_symmetricIco_linear_sub_linear_add_one_eq_zero (z : UpperHalfPlane) (m : ℤ) : ∑'[SummationFilter.symmetricIco ℤ] (n : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1)) = 0

theorem EisensteinSeries.tendsto_tsum_one_div_linear_sub_succ_eq (z : UpperHalfPlane) : Filter.Tendsto (fun (N : ℕ+) => ∑ n ∈ Finset.Ico (-↑↑N) ↑↑N, ∑' (m : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1))) Filter.atTop (nhds (-2 * ↑Real.pi * Complex.I / ↑z))

theorem EisensteinSeries.tsum_symmetricIco_tsum_sub_eq (z : UpperHalfPlane) : ∑'[SummationFilter.symmetricIco ℤ] (n : ℤ), ∑' (m : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1)) = -2 * ↑Real.pi * Complex.I / ↑z

theorem EisensteinSeries.tsum_tsum_symmetricIco_sub_eq (z : UpperHalfPlane) : ∑' (m : ℤ), ∑'[SummationFilter.symmetricIco ℤ] (n : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1)) = 0