SpherePacking.ModularForms.E2

source

noncomputable def G₂ :

UpperHalfPlane → ℂ

Compatibility alias for Mathlib's EisensteinSeries.G2.

Equations

G₂ = EisensteinSeries.G2

Instances For

source

noncomputable def E₂ :

UpperHalfPlane → ℂ

Compatibility alias for Mathlib's EisensteinSeries.E2.

Equations

E₂ = EisensteinSeries.E2

Instances For

source

noncomputable def D₂ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) :

UpperHalfPlane → ℂ

Compatibility alias for Mathlib's EisensteinSeries.D2.

Equations

D₂ γ = EisensteinSeries.D2 γ

Instances For

source

theorem D₂_apply (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (z : UpperHalfPlane) :

D₂ γ z = 2 * ↑Real.pi * Complex.I * ↑(↑γ 1 0) / (↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1))

source

theorem D2_one :

D₂ 1 = 0

source

theorem D2_mul (A B : Matrix.SpecialLinearGroup (Fin 2) ℤ) :

D₂ (A * B) = SlashAction.map 2 B (D₂ A) + D₂ B

source

theorem D2_inv (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) :

SlashAction.map 2 A⁻¹ (D₂ A) = -D₂ A⁻¹

source

theorem D2_T :

D₂ ModularGroup.T = 0

source

theorem D2_S (z : UpperHalfPlane) :

D₂ ModularGroup.S z = 2 * ↑Real.pi * Complex.I / ↑z

source

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)

source

theorem G2_periodic :

SlashAction.map 2 ModularGroup.T G₂ = G₂

source

theorem G₂_transform (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) :

SlashAction.map 2 γ G₂ = G₂ - D₂ γ

source

theorem E₂_periodic (z : UpperHalfPlane) :

E₂ (1 +ᵥ z) = E₂ z

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

source

theorem E₂_transform (z : UpperHalfPlane) :

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

source

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

source

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

source

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)

source

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