Documentation

LeanPool.LeanModularForms.Modularforms.E2

E2 #

source
noncomputable def G₂ :
UpperHalfPlane → ℂ

Compatibility alias for Mathlib's EisensteinSeries.G2.

Equations
Instances For
    source
    noncomputable def E₂ :
    UpperHalfPlane → ℂ

    Compatibility alias for Mathlib's EisensteinSeries.E2.

    Equations
    Instances For
      source
      noncomputable def D₂ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) :
      UpperHalfPlane → ℂ

      Compatibility alias for Mathlib's EisensteinSeries.D2.

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