def G₂ : UpperHalfPlane → ℂ

Compatibility alias for Mathlib's EisensteinSeries.G2.

Equations

• G₂ = EisensteinSeries.G2

def E₂ : UpperHalfPlane → ℂ

Compatibility alias for Mathlib's EisensteinSeries.E2.

Equations

• E₂ = EisensteinSeries.E2

def D₂ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : UpperHalfPlane → ℂ

Compatibility alias for Mathlib's EisensteinSeries.D2.

Equations

• D₂ γ z = 2 * ↑Real.pi * Complex.I * ↑(↑γ 1 0) / UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z

theorem D₂_apply (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (z : UpperHalfPlane) : D₂ γ z = 2 * ↑Real.pi * Complex.I * ↑(↑γ 1 0) / (↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1))

theorem D2_one : D₂ 1 = 0

theorem D2_mul (A B : Matrix.SpecialLinearGroup (Fin 2) ℤ) : D₂ (A * B) = SlashAction.map 2 B (D₂ A) + D₂ B

theorem D2_inv (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) : SlashAction.map 2 A⁻¹ (D₂ A) = -D₂ A⁻¹

theorem D2_T : D₂ ModularGroup.T = 0

theorem D2_S (z : UpperHalfPlane) : D₂ ModularGroup.S z = 2 * ↑Real.pi * Complex.I / ↑z

theorem G2_q_exp (z : UpperHalfPlane) : G₂ z = 2 * riemannZeta 2 - 8 * ↑Real.pi ^ 2 * ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma 1) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z)

theorem G2_periodic : SlashAction.map 2 ModularGroup.T G₂ = G₂

theorem G₂_transform (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : SlashAction.map 2 γ G₂ = G₂ - D₂ γ

theorem E₂_periodic (z : UpperHalfPlane) : E₂ (1 +ᵥ z) = E₂ z

E₂ is 1-periodic: E₂(z + 1) = E₂(z).

theorem E₂_transform (z : UpperHalfPlane) : SlashAction.map 2 ModularGroup.S E₂ z = E₂ z + 6 / (↑Real.pi * Complex.I * ↑z)

theorem E₂_slash_transform (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : SlashAction.map 2 γ E₂ = E₂ - (1 / (2 * riemannZeta 2)) • D₂ γ

E₂ transforms under SL(2,ℤ) as: E₂ ∣[2] γ = E₂ - α • D₂ γ where α = 1/(2ζ(2)).

theorem E₂_S_transform (z : UpperHalfPlane) : E₂ (ModularGroup.S • z) = ↑z ^ 2 * (E₂ z + 6 / (↑Real.pi * Complex.I * ↑z))

E₂ transforms under S as: E₂(-1/z) = z² · (E₂(z) + 6/(πIz)).

theorem tsum_eq_tsum_sigma (z : UpperHalfPlane) : ∑' (n : ℕ), (↑n + 1) * Complex.exp (2 * ↑Real.pi * Complex.I * (↑n + 1) * ↑z) / (1 - Complex.exp (2 * ↑Real.pi * Complex.I * (↑n + 1) * ↑z)) = ∑' (n : ℕ), ↑((ArithmeticFunction.sigma 1) (n + 1)) * Complex.exp (2 * ↑Real.pi * Complex.I * (↑n + 1) * ↑z)

theorem E₂_eq (z : UpperHalfPlane) : E₂ z = 1 - 24 * ∑' (n : ℕ+), ↑↑n * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z) / (1 - Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z))