Valence Formula Definitions

Definitions for the valence formula for SL₂(ℤ): elliptic points i and ρ, orbifold coefficients, the order of vanishing, and the canonical fundamental domain.

We use ModularGroup.fd (notation 𝒟) from mathlib for the standard fundamental domain.

def ellipticPointI' : UpperHalfPlane

The elliptic point i as an element of ℍ.

Equations

• ellipticPointI' = { coe := Complex.I, coe_im_pos := ellipticPointI'._proof_1 }

@[reducible, inline]

abbrev ellipticPointI : ℂ

The elliptic point i as a complex number.

Equations

• ellipticPointI = ↑ellipticPointI'

noncomputable def ellipticPointRho' : UpperHalfPlane

The elliptic point ρ = e^{2πi/3} = -1/2 + (√3/2)i as an element of ℍ.

Equations

• ellipticPointRho' = { coe := -1 / 2 + ↑√3 / 2 * Complex.I, coe_im_pos := ellipticPointRho'._proof_3 }

@[reducible, inline]

noncomputable abbrev ellipticPointRho : ℂ

The elliptic point ρ as a complex number.

Equations

• ellipticPointRho = ↑ellipticPointRho'

noncomputable def ellipticPointRhoPlusOne' : UpperHalfPlane

The T-translate ρ+1 = e^{πi/3} = 1/2 + (√3/2)i.

Equations

• ellipticPointRhoPlusOne' = { coe := 1 / 2 + ↑√3 / 2 * Complex.I, coe_im_pos := ellipticPointRhoPlusOne'._proof_1 }

@[reducible, inline]

noncomputable abbrev ellipticPointRhoPlusOne : ℂ

The T-translate ρ + 1 as a complex number.

Equations

• ellipticPointRhoPlusOne = ↑ellipticPointRhoPlusOne'

theorem ellipticPointRho_add_one_eq : ellipticPointRho + 1 = ellipticPointRhoPlusOne

theorem ellipticPointRhoPlusOne_norm : ‖ellipticPointRhoPlusOne‖ = 1

theorem ellipticPointRho_norm : ‖ellipticPointRho‖ = 1

theorem ellipticPointI_mem_fd : ellipticPointI' ∈ ModularGroup.fd

theorem ellipticPointRho_mem_fd : ellipticPointRho' ∈ ModularGroup.fd

theorem ellipticPointI_ne_rho : ellipticPointI' ≠ ellipticPointRho'

noncomputable def orderOfVanishingAt' (f : UpperHalfPlane → ℂ) (z : UpperHalfPlane) : ℤ

Order of vanishing of f at a point in ℍ.

Equations

• orderOfVanishingAt' f z = (meromorphicOrderAt (fun (w : ℂ) => if h : 0 < w.im then f { coe := w, coe_im_pos := h } else 0) ↑z).untop₀

noncomputable def orderAtCusp' {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) : ℤ

The order of vanishing at the cusp (in the q-expansion).

Equations

• orderAtCusp' f = ↑(UpperHalfPlane.qExpansion 1 ⇑f).order.toNat