Einstein series q-expansions

We give some identities for q-expansions of Eisenstein series that will be used in describing their q-expansions.

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