Modular forms #

This file defines modular forms and proves some basic properties about them. Including constructing the graded ring of modular forms.

We begin by defining modular forms and cusp forms as extension of SlashInvariantForms then we define the space of modular forms, cusp forms and prove that the product of two modular forms is a modular form.

source

def UpperHalfPlane.J :

GL (Fin 2) ℝ

The matrix [1, 0; 0, -1], which defines an anti-holomorphic involution of ℍ via τ ↦ -conj τ.

Equations

Instances For

source

theorem UpperHalfPlane.coe_J_smul (τ : UpperHalfPlane) :

↑(J • τ) = -(starRingEnd ℂ) ↑τ

source

theorem UpperHalfPlane.J_smul (τ : UpperHalfPlane) :

J • τ = ↑ofComplex (-(starRingEnd ℂ) ↑τ)

source

@[simp]

theorem UpperHalfPlane.val_J :

↑J = !![1, 0; 0, -1]

source

@[simp]

theorem UpperHalfPlane.J_sq :

J ^ 2 = 1

source

@[simp]

theorem UpperHalfPlane.det_J :

Matrix.GeneralLinearGroup.det J = -1

source

@[simp]

theorem UpperHalfPlane.sigma_J :

σ J = starRingEnd ℂ

source

@[simp]

theorem UpperHalfPlane.denom_J (τ : UpperHalfPlane) :

denom J ↑τ = -1

source

theorem MDifferentiable.slash {f : UpperHalfPlane → ℂ} (hf : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) f) (k : ℤ) (g : GL (Fin 2) ℝ) :

MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) (SlashAction.map ℂ k g f)

The weight k slash action of GL(2, ℝ) preserves holomorphic functions.

source

structure ModularForm (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (k : ℤ) extends SlashInvariantForm Γ k :

Type

These are SlashInvariantForm's that are holomorphic and bounded at infinity.

toFun : UpperHalfPlane → ℂ
slash_action_eq' (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : γ ∈ Γ → SlashAction.map ℂ k γ self.toFun = self.toFun
holo' : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⇑self.toSlashInvariantForm
bdd_at_infty' (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) : UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map ℂ k A ⇑self.toSlashInvariantForm)

Instances For

source

structure CuspForm (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (k : ℤ) extends SlashInvariantForm Γ k :

Type

These are SlashInvariantForms that are holomorphic and zero at infinity.

toFun : UpperHalfPlane → ℂ
slash_action_eq' (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : γ ∈ Γ → SlashAction.map ℂ k γ self.toFun = self.toFun
holo' : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⇑self.toSlashInvariantForm
zero_at_infty' (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) : UpperHalfPlane.IsZeroAtImInfty (SlashAction.map ℂ k A ⇑self.toSlashInvariantForm)

Instances For

source

class ModularFormClass (F : Type u_2) (Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))) (k : outParam ℤ) [FunLike F UpperHalfPlane ℂ] extends SlashInvariantFormClass F Γ k :

Prop

ModularFormClass F Γ k says that F is a type of bundled functions that extend SlashInvariantFormClass by requiring that the functions be holomorphic and bounded at infinity.

slash_action_eq (f : F) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : γ ∈ Γ → SlashAction.map ℂ k γ ⇑f = ⇑f
holo (f : F) : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⇑f
bdd_at_infty (f : F) (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) : UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map ℂ k A ⇑f)

Instances

source

class CuspFormClass (F : Type u_2) (Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))) (k : outParam ℤ) [FunLike F UpperHalfPlane ℂ] extends SlashInvariantFormClass F Γ k :

Prop

CuspFormClass F Γ k says that F is a type of bundled functions that extend SlashInvariantFormClass by requiring that the functions be holomorphic and zero at infinity.