Eisenstein series q-expansions

We give the q-expansion of Eisenstein series of weight k and level 1. In particular, we prove EisensteinSeries.q_expansion_bernoulli which says that for even k with 3 ≤ k Eisenstein series can we written as 1 - (2k / bernoulli k) ∑' n, σ_{k-1}(n) q^n where q = exp(2πiz) and σ_{k-1}(n) is the sum of the (k-1)-th powers of the divisors of n. We need k to be even so that the Eisenstein series are non-zero and we require k ≥ 3 so that the series converges absolutely.

The proof relies on the identity ∑' n : ℤ, 1 / (z + n) ^ (k + 1) = ((-2πi)^(k+1) / k!) ∑' n : ℕ, n^k q^n which comes from differentiating the expansion of π cot(πz) in terms of exponentials. Since our Eisenstein series are defined as sums over coprime integer pairs, we also need to relate these to sums over all pairs of integers, which is done in tsum_eisSummand_eq_riemannZeta_mul_eisensteinSeries. This then gives the q-expansion with a Riemann zeta factor, which we simplify using the formula for ζ(k) in terms of Bernoulli numbers to get the final result.

theorem summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp (k l : ℕ) {f : ℕ → ℂ} {p : ℝ} (hp : 0 < p) (hf : f =O[Filter.atTop] fun (n : ℕ) => ↑n ^ l) : SummableLocallyUniformlyOn (fun (n : ℕ) => f n • iteratedDerivWithin k (fun (z : ℂ) => Complex.exp (2 * ↑Real.pi * Complex.I * z / ↑p) ^ n) UpperHalfPlane.upperHalfPlaneSet) UpperHalfPlane.upperHalfPlaneSet

The infinte sum of k-th iterated derivative of the complex exponential multiplied by a function that grows polynomially is absolutely and uniformly convergent.

theorem summableLocallyUniformlyOn_iteratedDerivWithin_cexp (k : ℕ) : SummableLocallyUniformlyOn (fun (n : ℕ) => iteratedDerivWithin k (fun (z : ℂ) => Complex.exp (2 * ↑Real.pi * Complex.I * z) ^ n) UpperHalfPlane.upperHalfPlaneSet) UpperHalfPlane.upperHalfPlaneSet

This is a version of summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp for level one and q-expansion coefficients all 1.

theorem differentiableAt_iteratedDerivWithin_cexp (n a : ℕ) {s : Set ℂ} (hs : IsOpen s) {r : ℂ} (hr : r ∈ s) : DifferentiableAt ℂ (iteratedDerivWithin a (fun (z : ℂ) => Complex.exp (2 * ↑Real.pi * Complex.I * z) ^ n) s) r

theorem iteratedDerivWithin_tsum_cexp_eq (k : ℕ) (z : UpperHalfPlane) : iteratedDerivWithin k (fun (z : ℂ) => ∑' (n : ℕ), Complex.exp (2 * ↑Real.pi * Complex.I * z) ^ n) UpperHalfPlane.upperHalfPlaneSet ↑z = ∑' (n : ℕ), iteratedDerivWithin k (fun (s : ℂ) => Complex.exp (2 * ↑Real.pi * Complex.I * s) ^ n) UpperHalfPlane.upperHalfPlaneSet ↑z

theorem contDiffOn_tsum_cexp (k : ℕ∞) : ContDiffOn ℂ (↑k) (fun (z : ℂ) => ∑' (n : ℕ), Complex.exp (2 * ↑Real.pi * Complex.I * z) ^ n) UpperHalfPlane.upperHalfPlaneSet

theorem EisensteinSeries.qExpansion_identity {k : ℕ} (hk : 1 ≤ k) (z : UpperHalfPlane) : ∑' (n : ℤ), 1 / (↑z + ↑n) ^ (k + 1) = (-2 * ↑Real.pi * Complex.I) ^ (k + 1) / ↑k.factorial * ∑' (n : ℕ), ↑n ^ k * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ n

This is one key identity relating infinite series to q-expansions which shows that ∑' n, 1 / (z + n) ^ (k + 1) = ((-2 π I) ^ (k + 1) / k !) * ∑' n, n ^ k q ^n where q = cexp (2 π I z).

theorem summable_pow_mul_cexp (k : ℕ) (e : ℕ+) (z : UpperHalfPlane) : Summable fun (c : ℕ) => ↑c ^ k * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑e * ↑z) ^ c

theorem EisensteinSeries.qExpansion_identity_pnat {k : ℕ} (hk : 1 ≤ k) (z : UpperHalfPlane) : ∑' (n : ℤ), 1 / (↑z + ↑n) ^ (k + 1) = (-2 * ↑Real.pi * Complex.I) ^ (k + 1) / ↑k.factorial * ∑' (n : ℕ+), ↑↑n ^ k * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ↑n

This is a version of EisensteinSeries.qExpansion_identity for positive naturals, which shows that ∑' n, 1 / (z + n) ^ (k + 1) = ((-2 π I) ^ (k + 1) / k !) * ∑' n : ℕ+, n ^ k q ^n where q = cexp (2 π I z).

theorem summable_eisSummand {k : ℕ} (hk : 3 ≤ k) (z : UpperHalfPlane) : Summable fun (x : Fin 2 → ℤ) => EisensteinSeries.eisSummand (↑k) x z

theorem summable_prod_eisSummand {k : ℕ} (hk : 3 ≤ k) (z : UpperHalfPlane) : Summable fun (x : ℤ × ℤ) => EisensteinSeries.eisSummand ↑k ![x.1, x.2] z

theorem tsum_eisSummand_eq_tsum_sigma_mul_cexp_pow {k : ℕ} (hk : 3 ≤ k) (hk2 : Even k) (z : UpperHalfPlane) : ∑' (v : Fin 2 → ℤ), EisensteinSeries.eisSummand (↑k) v z = 2 * riemannZeta ↑k + 2 * ((-2 * ↑Real.pi * Complex.I) ^ k / ↑(k - 1).factorial) * ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma (k - 1)) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ↑n

theorem eisSummand_of_gammaSet_eq_divIntMap (k : ℤ) (z : UpperHalfPlane) {n : ℕ} (v : ↑(EisensteinSeries.gammaSet 1 n 0)) : EisensteinSeries.eisSummand k (↑v) z = (↑n ^ k)⁻¹ * EisensteinSeries.eisSummand k (EisensteinSeries.divIntMap ↑n ↑v) z

theorem tsum_eisSummand_eq_riemannZeta_mul_eisensteinSeries {k : ℕ} (hk : 3 ≤ k) (z : UpperHalfPlane) : ∑' (v : Fin 2 → ℤ), EisensteinSeries.eisSummand (↑k) v z = riemannZeta ↑k * eisensteinSeries 0 (↑k) z

theorem EisensteinSeries.q_expansion_riemannZeta {k : ℕ} (hk : 3 ≤ k) (hk2 : Even k) (z : UpperHalfPlane) : (ModularForm.E hk) z = 1 + (riemannZeta ↑k)⁻¹ * (-2 * ↑Real.pi * Complex.I) ^ k / ↑(k - 1).factorial * ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma (k - 1)) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ↑↑n

The q-Expansion of normalised Eisenstein series of level one with riemannZeta term.

theorem EisensteinSeries.q_expansion_bernoulli {k : ℕ} (hk : 3 ≤ k) (hk2 : Even k) (z : UpperHalfPlane) : (ModularForm.E hk) z = 1 - 2 * ↑k / ↑(bernoulli k) * ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma (k - 1)) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ↑↑n

The q-Expansion of normalised Eisenstein series of level one with bernoulli term.