def standardcongruencecondition : Fin 2 → ZMod ↑1

Equations

• standardcongruencecondition = 0

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

Equations

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

def gammaSetN (N : ℕ) : Set (Fin 2 → ℤ)

Equations

• gammaSetN N = {N} • EisensteinSeries.gammaSet 1 1 0

def gammaSetN_map (N : ℕ) (v : ↑(gammaSetN N)) : ↑(EisensteinSeries.gammaSet 1 1 0)

Equations

• gammaSetN_map N v = ⟨⋯.choose, ⋯⟩

theorem gammaSet_top_mem (v : Fin 2 → ℤ) : v ∈ EisensteinSeries.gammaSet 1 1 0 ↔ IsCoprime (v 0) (v 1)

theorem gammaSetN_map_eq (N : ℕ) (v : ↑(gammaSetN N)) : ↑v = N • ↑(gammaSetN_map N v)

def gammaSetN_Equiv (N : ℕ) (hN : N ≠ 0) : ↑(gammaSetN N) ≃ ↑(EisensteinSeries.gammaSet 1 1 0)

Equations

• gammaSetN_Equiv N hN = { toFun := fun (v : ↑(gammaSetN N)) => gammaSetN_map N v, invFun := fun (v : ↑(EisensteinSeries.gammaSet 1 1 0)) => ⟨N • ↑v, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem gammaSetN_eisSummand (k : ℤ) (z : UpperHalfPlane) (n : ℕ) (v : ↑(gammaSetN n)) : EisensteinSeries.eisSummand k (↑v) z = (↑n ^ k)⁻¹ * EisensteinSeries.eisSummand k (↑(gammaSetN_map n v)) z

def GammaSet_one_Equiv : (Fin 2 → ℤ) ≃ (n : ℕ) × ↑(gammaSetN n)

Equations

• One or more equations did not get rendered due to their size.

theorem q_exp_iden_2 (k : ℕ) (hk : 3 ≤ k) (hk2 : Even k) (z : UpperHalfPlane) : ∑' (x : ℤ × ℤ), 1 / (↑x.1 * ↑z + ↑x.2) ^ k = 2 * riemannZeta ↑k + 2 * ∑' (c : ℕ+) (d : ℤ), 1 / (↑↑c * ↑z + ↑d) ^ k

theorem EQ0 (k : ℕ) (z : UpperHalfPlane) : ∑' (x : Fin 2 → ℤ), 1 / (↑(x 0) * ↑z + ↑(x 1)) ^ k = ∑' (x : ℤ × ℤ), 1 / (↑x.1 * ↑z + ↑x.2) ^ k

theorem EQ1 (k : ℕ) (hk : 3 ≤ ↑k) (hk2 : Even k) (z : UpperHalfPlane) : ∑' (x : Fin 2 → ℤ), 1 / (↑(x 0) * ↑z + ↑(x 1)) ^ k = 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 EQ22 (k : ℕ) (hk : 3 ≤ ↑k) (z : UpperHalfPlane) : ∑' (x : Fin 2 → ℤ), EisensteinSeries.eisSummand (↑k) x z = riemannZeta ↑k * ∑' (c : ↑(EisensteinSeries.gammaSet 1 1 0)), EisensteinSeries.eisSummand (↑k) (↑c) z

theorem EQ2 (k : ℕ) (hk : 3 ≤ ↑k) (z : UpperHalfPlane) : ∑' (x : Fin 2 → ℤ), 1 / (↑(x 0) * ↑z + ↑(x 1)) ^ k = riemannZeta ↑k * ∑' (c : ↑(EisensteinSeries.gammaSet 1 1 0)), 1 / (↑(↑c 0) * ↑z + ↑(↑c 1)) ^ k

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)