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

Equations

• ModForm_mk Γ 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) : ModForm_mk Γ k f ≠ 0

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

Equations

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

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

Equations

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

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

Equations

• CuspForm_iso_CuspFormSubmodule Γ k = LinearEquiv.ofInjective (CuspForm_to_ModularForm Γ 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 = (CuspForm_to_ModularForm Γ 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

Equations

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

noncomputable def IsCuspForm_to_CuspForm (Γ : 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

Equations

• IsCuspForm_to_CuspForm Γ 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) : (IsCuspForm_to_CuspForm Γ 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) : (IsCuspForm_to_CuspForm Γ 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) (ModularFormClass.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) (ModularFormClass.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) (ModularFormClass.qExpansion 1 ⇑f) = 0