Documentation

SpherePacking.MagicFunction.b.Psi

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 ⟩

Instances For

noncomputable def h :

UpperHalfPlane → ℂ

Equations

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

Instances For

noncomputable def ψI :

UpperHalfPlane → ℂ

Equations

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

Instances For

noncomputable def ψT :

UpperHalfPlane → ℂ

Equations

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

Instances For

noncomputable def ψS :

UpperHalfPlane → ℂ

Equations

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

Instances For

noncomputable def ψI' (z : ℂ) :

Equations

ψI' z = if hz : 0 < z.im then ψI { coe := z, coe_im_pos := hz } else 0

Instances For

noncomputable def ψS' (z : ℂ) :

Equations

ψS' z = if hz : 0 < z.im then ψS { coe := z, coe_im_pos := hz } else 0

Instances For

noncomputable def ψT' (z : ℂ) :

Equations

ψT' z = if hz : 0 < z.im then ψT { coe := z, coe_im_pos := hz } else 0

Instances For

theorem ψI'_def {z : ℂ} (hz : 0 < z.im) :

ψI' z = ψI { coe := z, coe_im_pos := hz }

theorem ψS'_def {z : ℂ} (hz : 0 < z.im) :

ψS' z = ψS { coe := z, coe_im_pos := hz }

theorem ψT'_def {z : ℂ} (hz : 0 < z.im) :

ψT' z = ψT { coe := z, coe_im_pos := hz }

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 ψS_eq_neg_one_half_smul_G_div_disc :

ψS = (-1 / 2) • G / Δ

ψS in terms of the weight-10 form G and the discriminant: ψS = -G / (2Δ). This follows from ψS_eq', the Jacobi identity H₂ + H₄ = H₃, and Δ = (H₂H₃H₄)² / 256.

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

theorem ψI'_eq_ψI_of_mem {z : ℂ} (hz : 0 < z.im) :

ψI' z = ψI { coe := z, coe_im_pos := hz }

theorem ψS'_eq_ψS_of_mem {z : ℂ} (hz : 0 < z.im) :

ψS' z = ψS { coe := z, coe_im_pos := hz }

theorem ψT'_eq_ψT_of_mem {z : ℂ} (hz : 0 < z.im) :

ψT' z = ψT { coe := z, coe_im_pos := hz }

theorem ψT'_comp_z₁'_eq_ψT_comp_z₁'_of_mem {t : ℝ} (ht : t ∈ Set.Ioc 0 1) :

ψT' (MagicFunction.Parametrisations.z₁' t) = ψT { coe := MagicFunction.Parametrisations.z₁' t, coe_im_pos := ⋯ }

theorem ψS'_comp_z₁'_eq_ψS_comp_z₁'_of_mem {t : ℝ} (ht : t ∈ Set.Ioc 0 1) :

ψS' (MagicFunction.Parametrisations.z₁' t) = ψS { coe := MagicFunction.Parametrisations.z₁' t, coe_im_pos := ⋯ }

theorem ψI'_comp_z₁'_eq_ψI_comp_z₁'_of_mem {t : ℝ} (ht : t ∈ Set.Ioc 0 1) :

ψI' (MagicFunction.Parametrisations.z₁' t) = ψI { coe := MagicFunction.Parametrisations.z₁' t, coe_im_pos := ⋯ }

theorem ψT'_comp_z₂'_eq_ψT_comp_z₂'_of_mem {t : ℝ} (ht : t ∈ Set.Icc 0 1) :

ψT' (MagicFunction.Parametrisations.z₂' t) = ψT { coe := MagicFunction.Parametrisations.z₂' t, coe_im_pos := ⋯ }

theorem ψS'_comp_z₂'_eq_ψS_comp_z₂'_of_mem {t : ℝ} (ht : t ∈ Set.Icc 0 1) :

ψS' (MagicFunction.Parametrisations.z₂' t) = ψS { coe := MagicFunction.Parametrisations.z₂' t, coe_im_pos := ⋯ }

theorem ψI'_comp_z₂'_eq_ψI_comp_z₂'_of_mem {t : ℝ} (ht : t ∈ Set.Icc 0 1) :

ψI' (MagicFunction.Parametrisations.z₂' t) = ψI { coe := MagicFunction.Parametrisations.z₂' t, coe_im_pos := ⋯ }

theorem ψT'_comp_z₃'_eq_ψT_comp_z₃'_of_mem {t : ℝ} (ht : t ∈ Set.Ioc 0 1) :

ψT' (MagicFunction.Parametrisations.z₃' t) = ψT { coe := MagicFunction.Parametrisations.z₃' t, coe_im_pos := ⋯ }

theorem ψS'_comp_z₃'_eq_ψS_comp_z₃'_of_mem {t : ℝ} (ht : t ∈ Set.Ioc 0 1) :

ψS' (MagicFunction.Parametrisations.z₃' t) = ψS { coe := MagicFunction.Parametrisations.z₃' t, coe_im_pos := ⋯ }

theorem ψI'_comp_z₃'_eq_ψI_comp_z₃'_of_mem {t : ℝ} (ht : t ∈ Set.Ioc 0 1) :

ψI' (MagicFunction.Parametrisations.z₃' t) = ψI { coe := MagicFunction.Parametrisations.z₃' t, coe_im_pos := ⋯ }

theorem ψT'_comp_z₄'_eq_ψT_comp_z₄'_of_mem {t : ℝ} (ht : t ∈ Set.Icc 0 1) :

ψT' (MagicFunction.Parametrisations.z₄' t) = ψT { coe := MagicFunction.Parametrisations.z₄' t, coe_im_pos := ⋯ }

theorem ψS'_comp_z₄'_eq_ψS_comp_z₄'_of_mem {t : ℝ} (ht : t ∈ Set.Icc 0 1) :

ψS' (MagicFunction.Parametrisations.z₄' t) = ψS { coe := MagicFunction.Parametrisations.z₄' t, coe_im_pos := ⋯ }

theorem ψI'_comp_z₄'_eq_ψI_comp_z₄'_of_mem {t : ℝ} (ht : t ∈ Set.Icc 0 1) :

ψI' (MagicFunction.Parametrisations.z₄' t) = ψI { coe := MagicFunction.Parametrisations.z₄' t, coe_im_pos := ⋯ }

theorem ψT'_comp_z₅'_eq_ψT_comp_z₅'_of_mem {t : ℝ} (ht : t ∈ Set.Ioc 0 1) :

ψT' (MagicFunction.Parametrisations.z₅' t) = ψT { coe := MagicFunction.Parametrisations.z₅' t, coe_im_pos := ⋯ }

theorem ψS'_comp_z₅'_eq_ψS_comp_z₅'_of_mem {t : ℝ} (ht : t ∈ Set.Ioc 0 1) :

ψS' (MagicFunction.Parametrisations.z₅' t) = ψS { coe := MagicFunction.Parametrisations.z₅' t, coe_im_pos := ⋯ }

theorem ψI'_comp_z₅'_eq_ψI_comp_z₅'_of_mem {t : ℝ} (ht : t ∈ Set.Ioc 0 1) :

ψI' (MagicFunction.Parametrisations.z₅' t) = ψI { coe := MagicFunction.Parametrisations.z₅' t, coe_im_pos := ⋯ }

theorem ψT'_comp_z₆'_eq_ψT_comp_z₆'_of_mem {t : ℝ} (ht : t ∈ Set.Ici 1) :

ψT' (MagicFunction.Parametrisations.z₆' t) = ψT { coe := MagicFunction.Parametrisations.z₆' t, coe_im_pos := ⋯ }

theorem ψS'_comp_z₆'_eq_ψS_comp_z₆'_of_mem {t : ℝ} (ht : t ∈ Set.Ici 1) :

ψS' (MagicFunction.Parametrisations.z₆' t) = ψS { coe := MagicFunction.Parametrisations.z₆' t, coe_im_pos := ⋯ }

theorem ψI'_comp_z₆'_eq_ψI_comp_z₆'_of_mem {t : ℝ} (ht : t ∈ Set.Ici 1) :

ψI' (MagicFunction.Parametrisations.z₆' t) = ψI { coe := MagicFunction.Parametrisations.z₆' t, coe_im_pos := ⋯ }

theorem ψS_slash_ST_apply (z : UpperHalfPlane) :

SlashAction.map (-2) (ModularGroup.S * ModularGroup.T) ψS z = ψS { coe := -1 / (↑z + 1), coe_im_pos := ⋯ } * (↑z + 1) ^ 2

theorem ψS_slash_ST_apply' (z : UpperHalfPlane) :

SlashAction.map (-2) (ModularGroup.S * ModularGroup.T) ψS z = ψS' (-1 / (↑z + 1)) * (↑z + 1) ^ 2

theorem ψS_slash_S_apply (z : UpperHalfPlane) :

SlashAction.map (-2) ModularGroup.S ψS z = ψS { coe := -1 / ↑z, coe_im_pos := ⋯ } * ↑z ^ 2

theorem ψS_slash_S_apply' (z : UpperHalfPlane) :

SlashAction.map (-2) ModularGroup.S ψS z = ψS' (-1 / ↑z) * ↑z ^ 2

theorem ψS_slash_ST_explicit₁ {t : ℝ} (ht : t ∈ Set.Ioc 0 1) :

ψT' (MagicFunction.Parametrisations.z₁' t) = ψS' (-1 / (MagicFunction.Parametrisations.z₁' t + 1)) * (MagicFunction.Parametrisations.z₁' t + 1) ^ 2

theorem ψS_slash_ST_explicit₂ {t : ℝ} (ht : t ∈ Set.Icc 0 1) :

ψT' (MagicFunction.Parametrisations.z₂' t) = ψS' (-1 / (MagicFunction.Parametrisations.z₂' t + 1)) * (MagicFunction.Parametrisations.z₂' t + 1) ^ 2

theorem ψS_slash_ST_explicit₃ {t : ℝ} (ht : t ∈ Set.Ioc 0 1) :

ψT' (MagicFunction.Parametrisations.z₃' t) = ψS' (-1 / (MagicFunction.Parametrisations.z₃' t + 1)) * (MagicFunction.Parametrisations.z₃' t + 1) ^ 2

theorem ψS_slash_ST_explicit₄ {t : ℝ} (ht : t ∈ Set.Icc 0 1) :

ψT' (MagicFunction.Parametrisations.z₄' t) = ψS' (-1 / (MagicFunction.Parametrisations.z₄' t + 1)) * (MagicFunction.Parametrisations.z₄' t + 1) ^ 2

theorem ψS_slash_S_explicit₅ {t : ℝ} (ht : t ∈ Set.Ioc 0 1) :

ψI' (MagicFunction.Parametrisations.z₅' t) = ψS' (-1 / MagicFunction.Parametrisations.z₅' t) * MagicFunction.Parametrisations.z₅' t ^ 2

theorem ψS_slash_ST_explicit₆ {t : ℝ} (ht : t ∈ Set.Ici 1) :

ψT' (MagicFunction.Parametrisations.z₆' t) = ψS' (-1 / (MagicFunction.Parametrisations.z₆' t + 1)) * (MagicFunction.Parametrisations.z₆' t + 1) ^ 2