IsCuspForm

def ModFormMk (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (k : ℤ) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k) : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k

Views a cusp form as a modular form.

Equations

• ModFormMk Γ k f = { toFun := ⇑f, slash_action_eq' := ⋯, holo' := ⋯, bdd_at_cusps' := ⋯ }

theorem ModForm_mk_inj (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (k : ℤ) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k) (hf : f ≠ 0) : ModFormMk Γ k f ≠ 0

def CuspFormToModularForm (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (k : ℤ) : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k →ₗ[ℂ] ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k

The linear inclusion of cusp forms into modular forms.

Equations

• CuspFormToModularForm Γ k = { toFun := fun (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k) => ModFormMk Γ k f, map_add' := ⋯, map_smul' := ⋯ }

def CuspFormSubmodule (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (k : ℤ) : Submodule ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k)

The submodule of modular forms that are cusp forms.

Equations

• CuspFormSubmodule Γ k = (CuspFormToModularForm Γ k).range

noncomputable def CuspFormIsoCuspFormSubmodule (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (k : ℤ) : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k ≃ₗ[ℂ] ↥(CuspFormSubmodule Γ k)

The linear isomorphism between cusp forms and the cusp-form submodule.

Equations

• CuspFormIsoCuspFormSubmodule Γ k = LinearEquiv.ofInjective (CuspFormToModularForm Γ k) ⋯

theorem mem_CuspFormSubmodule (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k) (hf : f ∈ CuspFormSubmodule Γ k) : ∃ (g : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k), f = (CuspFormToModularForm Γ k) g

@[implicit_reducible, instance 100]

instance CuspFormSubmodule.funLike {k : ℤ} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} : FunLike (↥(CuspFormSubmodule Γ k)) UpperHalfPlane ℂ

Equations

• CuspFormSubmodule.funLike = { coe := fun (f : ↥(CuspFormSubmodule Γ k)) => (↑f).toFun, coe_injective := ⋯ }

instance instCuspFormClassSubtypeModularFormMapSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGLMemSubmoduleComplexCuspFormSubmodule (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (k : ℤ) : CuspFormClass (↥(CuspFormSubmodule Γ k)) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k

def IsCuspForm (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k) : Prop

The predicate that a modular form lies in the cusp-form submodule.

Equations

• IsCuspForm Γ k f = (f ∈ CuspFormSubmodule Γ k)

noncomputable def IsCuspFormToCuspForm (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k) (hf : IsCuspForm Γ k f) : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k

Promotes a modular form satisfying IsCuspForm to a cusp form.

Equations

• IsCuspFormToCuspForm Γ k f hf = ⋯.choose

theorem CuspForm_to_ModularForm_coe (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k) (hf : IsCuspForm Γ k f) : (IsCuspFormToCuspForm Γ k f hf).toSlashInvariantForm = f.toSlashInvariantForm

theorem CuspForm_to_ModularForm_Fun_coe (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k) (hf : IsCuspForm Γ k f) : (IsCuspFormToCuspForm Γ k f hf).toFun = f.toFun

noncomputable def cuspFormOfSIFTendstoZero {k : ℤ} (f_SIF : SlashInvariantForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (h_mdiff : MDiff f_SIF.toFun) (h_zero : Filter.Tendsto f_SIF.toFun UpperHalfPlane.atImInfty (nhds 0)) : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k

Build a CuspForm from a SlashInvariantForm that is holomorphic and tends to 0.

Equations

• cuspFormOfSIFTendstoZero f_SIF h_mdiff h_zero = { toSlashInvariantForm := f_SIF, holo' := h_mdiff, zero_at_cusps' := ⋯ }

noncomputable def cuspFormOfCoeffZero {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (h : (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 ⇑f) = 0) : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k

Build a CuspForm from a modular form whose q-expansion has vanishing constant term.

Equations

• cuspFormOfCoeffZero f h = { toSlashInvariantForm := f.toSlashInvariantForm, holo' := ⋯, zero_at_cusps' := ⋯ }

theorem IsCuspForm_iff_coeffZero_eq_zero (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) : IsCuspForm (CongruenceSubgroup.Gamma 1) k f ↔ (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 ⇑f) = 0

theorem CuspFormSubmodule_mem_iff_coeffZero_eq_zero (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) : f ∈ CuspFormSubmodule (CongruenceSubgroup.Gamma 1) k ↔ (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 ⇑f) = 0