The ψ Functions

In this file, we define the functions ψI, ψT and ψS that are defined using the Jacobi theta functions and are used in the definition of the -1-eigenfunction b.

def ModularGroup.I : Matrix.SpecialLinearGroup (Fin 2) ℤ

Equations

• ModularGroup.I = ⟨!![1, 0; 0, 1], ModularGroup.I._proof_1⟩

def h : UpperHalfPlane → ℂ

Equations

• h = 128 • (⇑H₃_MF + ⇑H₄_MF) / ⇑H₂_MF ^ 2

def ψI : UpperHalfPlane → ℂ

Equations

• ψI = h - SlashAction.map (-2) (ModularGroup.S * ModularGroup.T) h

def ψT : UpperHalfPlane → ℂ

Equations

• ψT = SlashAction.map (-2) ModularGroup.T ψI

def ψS : UpperHalfPlane → ℂ

Equations

• ψS = SlashAction.map (-2) ModularGroup.S ψI

def ψI' (z : ℂ) : ℂ

Equations

• ψI' z = if hz : 0 < z.im then ψI ⟨z, hz⟩ else 0

def ψS' (z : ℂ) : ℂ

Equations

• ψS' z = if hz : 0 < z.im then ψS ⟨z, hz⟩ else 0

def ψT' (z : ℂ) : ℂ

Equations

• ψT' z = if hz : 0 < z.im then ψT ⟨z, hz⟩ else 0

theorem ψI_eq : ψI = 128 • ((⇑H₃_MF + ⇑H₄_MF) / ⇑H₂_MF ^ 2 + (⇑H₄_MF - ⇑H₂_MF) / ⇑H₃_MF ^ 2)

theorem ψT_eq : ψT = 128 * ((⇑H₃_MF + ⇑H₄_MF) / ⇑H₂_MF ^ 2 + (⇑H₂_MF + ⇑H₃_MF) / ⇑H₄_MF ^ 2)

theorem ψS_eq' : ψS = 128 * ((⇑H₄_MF - ⇑H₂_MF) / ⇑H₃_MF ^ 2 - (⇑H₂_MF + ⇑H₃_MF) / ⇑H₄_MF ^ 2)

theorem ψS_eq : ψS = 128 * (-((⇑H₂_MF + ⇑H₃_MF) / ⇑H₄_MF ^ 2) - (⇑H₂_MF - ⇑H₄_MF) / ⇑H₃_MF ^ 2)

theorem ψT_slash_T : SlashAction.map (-2) ModularGroup.T ψT = ψI

theorem ψS_slash_S : SlashAction.map (-2) ModularGroup.S ψS = ψI

theorem ψS_slash_ST : SlashAction.map (-2) (ModularGroup.S * ModularGroup.T) ψS = ψT

theorem ψS_slash_T : SlashAction.map (-2) ModularGroup.T ψS = -ψS

theorem ψT_slash_S : SlashAction.map (-2) ModularGroup.S ψT = -ψT

theorem ψI_slash_TS : SlashAction.map (-2) (ModularGroup.T * ModularGroup.S) ψI = -ψT

theorem ψS_slash_STS : SlashAction.map (-2) (ModularGroup.S * ModularGroup.T * ModularGroup.S) ψS = -ψT

theorem ψS_slash_TSTS : SlashAction.map (-2) (ModularGroup.T * ModularGroup.S * ModularGroup.T * ModularGroup.S) ψS = ψT