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' := ⋯ }

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

Equations

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

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

@[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)

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

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

theorem IsCuspForm_of_SIF_tendsto_zero {k : ℤ} (f_SIF : SlashInvariantForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (h_mdiff : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) f_SIF.toFun) (h_zero : Filter.Tendsto f_SIF.toFun UpperHalfPlane.atImInfty (nhds 0)) : ∃ (f_MF : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k), IsCuspForm (CongruenceSubgroup.Gamma 1) k f_MF ∧ ∀ (z : UpperHalfPlane), f_MF z = f_SIF.toFun z

Build a cusp form from a SlashInvariantForm that's MDifferentiable and tends to zero at infinity.

This is a common pattern for proving cusp form membership: if a slash-invariant function vanishes at i∞, then it vanishes at all cusps (by slash invariance), hence is a cusp form.