def standardcongruencecondition : Fin 2 → ZMod ↑1

Equations

• standardcongruencecondition = 0

noncomputable def E (k : ℤ) (hk : 3 ≤ k) : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k

Equations

• E k hk = (1 / 2) • ModularForm.eisensteinSeriesMF hk standardcongruencecondition

theorem E_k_q_expansion (k : ℕ) (hk : 3 ≤ ↑k) (hk2 : Even k) (z : UpperHalfPlane) : (E (↑k) hk) z = 1 + 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)