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.

def UpperHalfPlane.J : GL (Fin 2) ℝ

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

theorem UpperHalfPlane.coe_J_smul (τ : UpperHalfPlane) : ↑(J • τ) = -(starRingEnd ℂ) ↑τ

theorem UpperHalfPlane.J_smul (τ : UpperHalfPlane) : J • τ = ↑ofComplex (-(starRingEnd ℂ) ↑τ)

@[simp]

theorem UpperHalfPlane.val_J : ↑J = !![-1, 0; 0, 1]

@[simp]

theorem UpperHalfPlane.J_sq : J ^ 2 = 1

@[simp]

theorem UpperHalfPlane.det_J : Matrix.GeneralLinearGroup.det J = -1

@[simp]

theorem UpperHalfPlane.sigma_J : σ J = starRingEnd ℂ

@[simp]

theorem UpperHalfPlane.denom_J (τ : UpperHalfPlane) : denom J ↑τ = 1

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.

structure ModularForm (Γ : Subgroup (GL (Fin 2) ℝ)) (k : ℤ) extends SlashInvariantForm Γ k : Type

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

• toFun : UpperHalfPlane → ℂ
• slash_action_eq' (γ : GL (Fin 2) ℝ) : γ ∈ Γ → SlashAction.map k γ self.toFun = self.toFun
• holo' : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⇑self.toSlashInvariantForm
• bdd_at_cusps' {c : OnePoint ℝ} (hc : IsCusp c Γ) : c.IsBoundedAt self.toFun k

structure CuspForm (Γ : Subgroup (GL (Fin 2) ℝ)) (k : ℤ) extends SlashInvariantForm Γ k : Type

These are SlashInvariantForms that are holomorphic and zero at infinity.

• toFun : UpperHalfPlane → ℂ
• slash_action_eq' (γ : GL (Fin 2) ℝ) : γ ∈ Γ → SlashAction.map k γ self.toFun = self.toFun
• holo' : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⇑self.toSlashInvariantForm
• zero_at_cusps' {c : OnePoint ℝ} (hc : IsCusp c Γ) : c.IsZeroAt self.toFun k

class ModularFormClass (F : Type u_2) (Γ : outParam (Subgroup (GL (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 all cusps.

• slash_action_eq (f : F) (γ : GL (Fin 2) ℝ) : γ ∈ Γ → SlashAction.map k γ ⇑f = ⇑f
• holo (f : F) : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⇑f
• bdd_at_cusps (f : F) {c : OnePoint ℝ} (hc : IsCusp c Γ) : c.IsBoundedAt (⇑f) k

class CuspFormClass (F : Type u_2) (Γ : outParam (Subgroup (GL (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 all cusps.

• slash_action_eq (f : F) (γ : GL (Fin 2) ℝ) : γ ∈ Γ → SlashAction.map k γ ⇑f = ⇑f
• holo (f : F) : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⇑f
• zero_at_cusps (f : F) {c : OnePoint ℝ} (hc : IsCusp c Γ) : c.IsZeroAt (⇑f) k

@[instance 100]

instance ModularForm.funLike (Γ : Subgroup (GL (Fin 2) ℝ)) (k : ℤ) : FunLike (ModularForm Γ k) UpperHalfPlane ℂ

@[instance 100]

instance ModularFormClass.modularForm (Γ : Subgroup (GL (Fin 2) ℝ)) (k : ℤ) : ModularFormClass (ModularForm Γ k) Γ k

theorem ModularFormClass.continuous {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_2} [FunLike F UpperHalfPlane ℂ] [ModularFormClass F Γ k] (f : F) : Continuous ⇑f

@[instance 100]

instance CuspForm.funLike (Γ : Subgroup (GL (Fin 2) ℝ)) (k : ℤ) : FunLike (CuspForm Γ k) UpperHalfPlane ℂ

@[instance 100]

instance CuspFormClass.cuspForm (Γ : Subgroup (GL (Fin 2) ℝ)) (k : ℤ) : CuspFormClass (CuspForm Γ k) Γ k

theorem ModularForm.toFun_eq_coe {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (f : ModularForm Γ k) : f.toFun = ⇑f

@[simp]

theorem ModularForm.toSlashInvariantForm_coe {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (f : ModularForm Γ k) : ⇑f.toSlashInvariantForm = ⇑f

theorem CuspForm.toFun_eq_coe {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {f : CuspForm Γ k} : f.toFun = ⇑f

@[simp]

theorem CuspForm.toSlashInvariantForm_coe {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (f : CuspForm Γ k) : ⇑f.toSlashInvariantForm = ⇑f

theorem ModularForm.ext {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {f g : ModularForm Γ k} (h : ∀ (x : UpperHalfPlane), f x = g x) : f = g

theorem ModularForm.ext_iff {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {f g : ModularForm Γ k} : f = g ↔ ∀ (x : UpperHalfPlane), f x = g x

theorem CuspForm.ext {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {f g : CuspForm Γ k} (h : ∀ (x : UpperHalfPlane), f x = g x) : f = g

theorem CuspForm.ext_iff {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {f g : CuspForm Γ k} : f = g ↔ ∀ (x : UpperHalfPlane), f x = g x

def ModularForm.copy {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (f : ModularForm Γ k) (f' : UpperHalfPlane → ℂ) (h : f' = ⇑f) : ModularForm Γ k

Copy of a ModularForm with a new toFun equal to the old one. Useful to fix definitional equalities.

def CuspForm.copy {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (f : CuspForm Γ k) (f' : UpperHalfPlane → ℂ) (h : f' = ⇑f) : CuspForm Γ k

Copy of a CuspForm with a new toFun equal to the old one. Useful to fix definitional equalities.

instance ModularForm.add {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} : Add (ModularForm Γ k)

@[simp]

theorem ModularForm.coe_add {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (f g : ModularForm Γ k) : ⇑(f + g) = ⇑f + ⇑g

@[simp]

theorem ModularForm.add_apply {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (f g : ModularForm Γ k) (z : UpperHalfPlane) : (f + g) z = f z + g z

instance ModularForm.instZero {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} : Zero (ModularForm Γ k)

@[simp]

theorem ModularForm.coe_zero {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} : ⇑0 = 0

@[simp]

theorem ModularForm.zero_apply {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (z : UpperHalfPlane) : 0 z = 0

@[simp]

theorem ModularForm.coe_eq_zero_iff {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (f : ModularForm Γ k) : ⇑f = 0 ↔ f = 0

theorem ModularForm.instIsScalarTowerComplex {α : Type u_1} [SMul α ℝ] [SMul α ℂ] [IsScalarTower α ℝ ℂ] : IsScalarTower α ℂ ℂ

instance ModularForm.instSMulℝ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {α : Type u_1} [SMul α ℝ] [SMul α ℂ] [IsScalarTower α ℝ ℂ] : SMul α (ModularForm Γ k)

@[simp]

theorem ModularForm.coe_smul {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {α : Type u_1} [SMul α ℝ] [SMul α ℂ] [IsScalarTower α ℝ ℂ] (f : ModularForm Γ k) (n : α) : ⇑(n • f) = n • ⇑f

@[simp]

theorem ModularForm.smul_apply {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {α : Type u_1} [SMul α ℝ] [SMul α ℂ] [IsScalarTower α ℝ ℂ] (f : ModularForm Γ k) (n : α) (z : UpperHalfPlane) : (n • f) z = n • f z

instance ModularForm.instSMulℂ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {α : Type u_1} [SMul α ℂ] [IsScalarTower α ℂ ℂ] [Γ.HasDetOne] : SMul α (ModularForm Γ k)

@[simp]

theorem ModularForm.IsGLPos.coe_smul {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {α : Type u_1} [SMul α ℂ] [IsScalarTower α ℂ ℂ] [Γ.HasDetOne] (f : ModularForm Γ k) (n : α) : ⇑(n • f) = n • ⇑f

@[simp]

theorem ModularForm.IsGLPos.smul_apply {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {α : Type u_1} [SMul α ℂ] [IsScalarTower α ℂ ℂ] [Γ.HasDetOne] (f : ModularForm Γ k) (n : α) (z : UpperHalfPlane) : (n • f) z = n • f z

instance ModularForm.instNeg {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} : Neg (ModularForm Γ k)

@[simp]

theorem ModularForm.coe_neg {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (f : ModularForm Γ k) : ⇑(-f) = -⇑f

@[simp]

theorem ModularForm.neg_apply {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (f : ModularForm Γ k) (z : UpperHalfPlane) : (-f) z = -f z

instance ModularForm.instSub {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} : Sub (ModularForm Γ k)

@[simp]

theorem ModularForm.coe_sub {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (f g : ModularForm Γ k) : ⇑(f - g) = ⇑f - ⇑g

@[simp]

theorem ModularForm.sub_apply {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (f g : ModularForm Γ k) (z : UpperHalfPlane) : (f - g) z = f z - g z

instance ModularForm.instAddCommGroup {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} : AddCommGroup (ModularForm Γ k)

def ModularForm.coeHom {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} : ModularForm Γ k →+ UpperHalfPlane → ℂ

Additive coercion from ModularForm to ℍ → ℂ.

@[simp]

theorem ModularForm.coeHom_apply {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (f : ModularForm Γ k) (a : UpperHalfPlane) : coeHom f a = f a

instance ModularForm.instModuleReal {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} : Module ℝ (ModularForm Γ k)

instance ModularForm.instModuleComplexOfHasDetOneFinOfNatNatReal {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] : Module ℂ (ModularForm Γ k)

instance ModularForm.instInhabited {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} : Inhabited (ModularForm Γ k)

def ModularForm.mul {Γ : Subgroup (GL (Fin 2) ℝ)} {k_1 k_2 : ℤ} [Γ.HasDetPlusMinusOne] (f : ModularForm Γ k_1) (g : ModularForm Γ k_2) : ModularForm Γ (k_1 + k_2)

The modular form of weight k_1 + k_2 given by the product of two modular forms of weights k_1 and k_2.

@[simp]

theorem ModularForm.coe_mul {Γ : Subgroup (GL (Fin 2) ℝ)} {k_1 k_2 : ℤ} [Γ.HasDetPlusMinusOne] (f : ModularForm Γ k_1) (g : ModularForm Γ k_2) : ⇑(f.mul g) = ⇑f * ⇑g

@[deprecated ModularForm.coe_mul (since := "2025-12-06")]

theorem ModularForm.mul_coe {Γ : Subgroup (GL (Fin 2) ℝ)} {k_1 k_2 : ℤ} [Γ.HasDetPlusMinusOne] (f : ModularForm Γ k_1) (g : ModularForm Γ k_2) : ⇑(f.mul g) = ⇑f * ⇑g

Alias of ModularForm.coe_mul.

def ModularForm.const {Γ : Subgroup (GL (Fin 2) ℝ)} (x : ℂ) [Γ.HasDetOne] : ModularForm Γ 0

The constant function with value x : ℂ as a modular form of weight 0 and any level.

@[simp]

theorem ModularForm.coe_const {Γ : Subgroup (GL (Fin 2) ℝ)} (x : ℂ) [Γ.HasDetOne] : ⇑(const x) = Function.const UpperHalfPlane x

@[deprecated ModularForm.coe_const (since := "2025-12-06")]

theorem ModularForm.const_toFun {Γ : Subgroup (GL (Fin 2) ℝ)} (x : ℂ) [Γ.HasDetOne] : ⇑(const x) = Function.const UpperHalfPlane x

Alias of ModularForm.coe_const.

@[simp]

theorem ModularForm.const_apply {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] (x : ℂ) (τ : UpperHalfPlane) : (const x) τ = x

def ModularForm.constℝ {Γ : Subgroup (GL (Fin 2) ℝ)} (x : ℝ) [Γ.HasDetPlusMinusOne] : ModularForm Γ 0

The constant function with value x : ℂ as a modular form of weight 0 and any level.

@[simp]

theorem ModularForm.coe_constℝ {Γ : Subgroup (GL (Fin 2) ℝ)} (x : ℝ) [Γ.HasDetPlusMinusOne] : ⇑(constℝ x) = Function.const UpperHalfPlane ↑x

@[deprecated ModularForm.coe_constℝ (since := "2025-12-06")]

theorem ModularForm.constℝ_toFun {Γ : Subgroup (GL (Fin 2) ℝ)} (x : ℝ) [Γ.HasDetPlusMinusOne] : ⇑(constℝ x) = Function.const UpperHalfPlane ↑x

Alias of ModularForm.coe_constℝ.

@[simp]

theorem ModularForm.constℝ_apply {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] (x : ℝ) (τ : UpperHalfPlane) : (constℝ x) τ = ↑x

instance ModularForm.instOneOfNatIntOfHasDetPlusMinusOneFinNatReal {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] : One (ModularForm Γ 0)

@[simp]

theorem ModularForm.one_coe_eq_one {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] : ⇑1 = 1

instance ModularForm.instNatCastOfNatIntOfHasDetPlusMinusOneFinNatReal {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] : NatCast (ModularForm Γ 0)

@[simp]

theorem ModularForm.coe_natCast {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] (n : ℕ) : ⇑↑n = ↑n

theorem ModularForm.toSlashInvariantForm_natCast {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] (n : ℕ) : (↑n).toSlashInvariantForm = ↑n

instance ModularForm.instIntCastOfNatIntOfHasDetPlusMinusOneFinNatReal {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] : IntCast (ModularForm Γ 0)

@[simp]

theorem ModularForm.coe_intCast {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] (z : ℤ) : ⇑↑z = ↑z

theorem ModularForm.toSlashInvariantForm_intCast {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] (z : ℤ) : (↑z).toSlashInvariantForm = ↑z

instance CuspForm.hasAdd {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} : Add (CuspForm Γ k)

@[simp]

theorem CuspForm.coe_add {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (f g : CuspForm Γ k) : ⇑(f + g) = ⇑f + ⇑g

@[simp]

theorem CuspForm.add_apply {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (f g : CuspForm Γ k) (z : UpperHalfPlane) : (f + g) z = f z + g z

instance CuspForm.instZero {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} : Zero (CuspForm Γ k)

@[simp]

theorem CuspForm.coe_zero {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} : ⇑0 = 0

@[simp]

theorem CuspForm.zero_apply {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (z : UpperHalfPlane) : 0 z = 0

theorem CuspForm.instIsScalarTowerComplex {α : Type u_2} [SMul α ℝ] [SMul α ℂ] [IsScalarTower α ℝ ℂ] : IsScalarTower α ℂ ℂ

instance CuspForm.instSMul {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {α : Type u_2} [SMul α ℝ] [SMul α ℂ] [IsScalarTower α ℝ ℂ] : SMul α (CuspForm Γ k)

@[simp]

theorem CuspForm.coe_smul {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {α : Type u_2} [SMul α ℝ] [SMul α ℂ] [IsScalarTower α ℝ ℂ] (f : CuspForm Γ k) (n : α) : ⇑(n • f) = n • ⇑f

@[simp]

theorem CuspForm.smul_apply {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {α : Type u_2} [SMul α ℝ] [SMul α ℂ] [IsScalarTower α ℝ ℂ] (f : CuspForm Γ k) (n : α) {z : UpperHalfPlane} : (n • f) z = n • f z

instance CuspForm.IsGLPos.instSMul {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {α : Type u_2} [SMul α ℂ] [IsScalarTower α ℂ ℂ] [Γ.HasDetOne] : SMul α (CuspForm Γ k)

@[simp]

theorem CuspForm.IsGLPos.coe_smul {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {α : Type u_2} [SMul α ℂ] [IsScalarTower α ℂ ℂ] [Γ.HasDetOne] (f : CuspForm Γ k) (n : α) : ⇑(n • f) = n • ⇑f

@[simp]

theorem CuspForm.IsGLPos.smul_apply {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {α : Type u_2} [SMul α ℂ] [IsScalarTower α ℂ ℂ] [Γ.HasDetOne] (f : CuspForm Γ k) (n : α) {z : UpperHalfPlane} : (n • f) z = n • f z

instance CuspForm.instNeg {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} : Neg (CuspForm Γ k)

@[simp]

theorem CuspForm.coe_neg {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (f : CuspForm Γ k) : ⇑(-f) = -⇑f

@[simp]

theorem CuspForm.neg_apply {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (f : CuspForm Γ k) (z : UpperHalfPlane) : (-f) z = -f z

instance CuspForm.instSub {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} : Sub (CuspForm Γ k)

@[simp]

theorem CuspForm.coe_sub {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (f g : CuspForm Γ k) : ⇑(f - g) = ⇑f - ⇑g

@[simp]

theorem CuspForm.sub_apply {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (f g : CuspForm Γ k) (z : UpperHalfPlane) : (f - g) z = f z - g z

instance CuspForm.instAddCommGroup {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} : AddCommGroup (CuspForm Γ k)

def CuspForm.coeHom {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} : CuspForm Γ k →+ UpperHalfPlane → ℂ

Additive coercion from CuspForm to ℍ → ℂ.

@[simp]

theorem CuspForm.coeHom_apply {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (f : CuspForm Γ k) (a : UpperHalfPlane) : coeHom f a = f a

instance CuspForm.instModuleReal {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} : Module ℝ (CuspForm Γ k)

instance CuspForm.instModuleComplexOfHasDetOneFinOfNatNatReal {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] : Module ℂ (CuspForm Γ k)

instance CuspForm.instInhabited {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} : Inhabited (CuspForm Γ k)

@[instance 99]

instance CuspForm.instModularFormClassOfCuspFormClass {F : Type u_1} {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [FunLike F UpperHalfPlane ℂ] [CuspFormClass F Γ k] : ModularFormClass F Γ k

def ModularForm.mcast {a b : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} (h : a = b) (f : ModularForm Γ a) : ModularForm Γ b

Cast for modular forms, which is useful for avoiding Heqs.

theorem ModularForm.gradedMonoid_eq_of_cast {Γ : Subgroup (GL (Fin 2) ℝ)} {a b : GradedMonoid (ModularForm Γ)} (h : a.fst = b.fst) (h2 : mcast h a.snd = b.snd) : a = b

instance ModularForm.instGOneIntOfHasDetPlusMinusOneFinOfNatNatReal (Γ : Subgroup (GL (Fin 2) ℝ)) [Γ.HasDetPlusMinusOne] : GradedMonoid.GOne (ModularForm Γ)

instance ModularForm.instGMulIntOfHasDetPlusMinusOneFinOfNatNatReal (Γ : Subgroup (GL (Fin 2) ℝ)) [Γ.HasDetPlusMinusOne] : GradedMonoid.GMul (ModularForm Γ)

instance ModularForm.instGCommRing (Γ : Subgroup (GL (Fin 2) ℝ)) [Γ.HasDetPlusMinusOne] : DirectSum.GCommRing (ModularForm Γ)

instance ModularForm.instGAlgebra (Γ : Subgroup (GL (Fin 2) ℝ)) [Γ.HasDetOne] : DirectSum.GAlgebra ℂ (ModularForm Γ)

def ModularForm.prod {ι : Type} {s : Finset ι} {k : ι → ℤ} (m : ℤ) (hm : m = ∑ i ∈ s, k i) {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] (F : (i : ι) → ModularForm Γ (k i)) : ModularForm Γ m

Given ModularForm's F i of weight k i for i : ι, define the form which as a function is a product of those indexed by s : Finset ι with weight m = ∑ i ∈ s, k i.

@[simp]

theorem ModularForm.coe_prod {ι : Type} {s : Finset ι} {k : ι → ℤ} (m : ℤ) (hm : m = ∑ i ∈ s, k i) {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] (F : (i : ι) → ModularForm Γ (k i)) : ⇑(prod m hm F) = ∏ i ∈ s, ⇑(F i)

def ModularForm.prodEqualWeights {ι : Type} {s : Finset ι} {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] (F : ι → ModularForm Γ k) : ModularForm Γ (↑s.card * k)

Given ModularForm's F i of weight k, define the form which as a function is a product of those indexed by s : Finset ι with weight #s * k.

@[simp]

theorem ModularForm.coe_prodEqualWeights {ι : Type} {s : Finset ι} {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] (F : ι → ModularForm Γ k) : ⇑(prodEqualWeights F) = ∏ i ∈ s, ⇑(F i)

noncomputable def ModularForm.translate {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (f : F) [ModularFormClass F Γ k] (g : GL (Fin 2) ℝ) : ModularForm (ConjAct.toConjAct g⁻¹ • Γ) k

Translating a ModularForm by GL(2, ℝ), to obtain a new ModularForm.

@[simp]

theorem ModularForm.coe_translate {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (f : F) [ModularFormClass F Γ k] (g : GL (Fin 2) ℝ) : ⇑(translate f g) = SlashAction.map k g ⇑f

noncomputable def CuspForm.translate {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (f : F) [CuspFormClass F Γ k] (g : GL (Fin 2) ℝ) : CuspForm (ConjAct.toConjAct g⁻¹ • Γ) k

Translating a CuspForm by SL(2, ℤ), to obtain a new CuspForm.

@[simp]

theorem CuspForm.coe_translate {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (f : F) [CuspFormClass F Γ k] (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) : ⇑(translate f (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g))) = SlashAction.map k g ⇑f

instance instFactIsCuspInftyRealOfIsArithmetic {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] : Fact (IsCusp OnePoint.infty Γ)

theorem ModularFormClass.bdd_at_infty {k : ℤ} {F : Type u_1} {Γ : Subgroup (GL (Fin 2) ℝ)} [FunLike F UpperHalfPlane ℂ] (f : F) [ModularFormClass F Γ k] [Fact (IsCusp OnePoint.infty Γ)] : UpperHalfPlane.IsBoundedAtImInfty ⇑f

theorem CuspFormClass.zero_at_infty {k : ℤ} {F : Type u_1} {Γ : Subgroup (GL (Fin 2) ℝ)} [FunLike F UpperHalfPlane ℂ] (f : F) [CuspFormClass F Γ k] [Fact (IsCusp OnePoint.infty Γ)] : UpperHalfPlane.IsZeroAtImInfty ⇑f

theorem ModularFormClass.bdd_at_infty_slash {k : ℤ} {F : Type u_1} {Γ : Subgroup (GL (Fin 2) ℝ)} [FunLike F UpperHalfPlane ℂ] (f : F) [Γ.IsArithmetic] (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) [ModularFormClass F Γ k] : UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map k g ⇑f)

theorem CuspFormClass.zero_at_infty_slash {k : ℤ} {F : Type u_1} {Γ : Subgroup (GL (Fin 2) ℝ)} [FunLike F UpperHalfPlane ℂ] (f : F) [Γ.IsArithmetic] (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) [CuspFormClass F Γ k] : UpperHalfPlane.IsZeroAtImInfty (SlashAction.map k g ⇑f)