Modular forms #
This file defines modular forms and proves some basic properties about them.
We begin by defining modular forms and cusp forms as extension of SlashInvariantForm
s then we
define the space of modular forms, cusp forms and prove that the product of two modular forms is a
modular form.
- toFun : UpperHalfPlane → ℂ
- slash_action_eq' : ∀ (γ : { x // x ∈ Γ }), SlashAction.map ℂ k γ s.toFun = s.toFun
- holo' : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ↑s.toSlashInvariantForm
- bdd_at_infty' : ∀ (A : Matrix.SpecialLinearGroup (Fin 2) ℤ), UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map ℂ k A ↑s.toSlashInvariantForm)
These are SlashInvariantForm
's that are holomophic and bounded at infinity.
Instances For
- toFun : UpperHalfPlane → ℂ
- slash_action_eq' : ∀ (γ : { x // x ∈ Γ }), SlashAction.map ℂ k γ s.toFun = s.toFun
- holo' : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ↑s.toSlashInvariantForm
- zero_at_infty' : ∀ (A : Matrix.SpecialLinearGroup (Fin 2) ℤ), UpperHalfPlane.IsZeroAtImInfty (SlashAction.map ℂ k A ↑s.toSlashInvariantForm)
These are SlashInvariantForm
s that are holomophic and zero at infinity.
Instances For
- coe : F → UpperHalfPlane → ℂ
- coe_injective' : Function.Injective FunLike.coe
- slash_action_eq : ∀ (f : F) (γ : { x // x ∈ Γ }), 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)
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.
Instances
- coe : F → UpperHalfPlane → ℂ
- coe_injective' : Function.Injective FunLike.coe
- slash_action_eq : ∀ (f : F) (γ : { x // x ∈ Γ }), SlashAction.map ℂ k γ ↑f = ↑f
- holo : ∀ (f : F), MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ↑f
- zero_at_infty : ∀ (f : F) (A : Matrix.SpecialLinearGroup (Fin 2) ℤ), UpperHalfPlane.IsZeroAtImInfty (SlashAction.map ℂ k A ↑f)
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.
Instances
Copy of a ModularForm
with a new toFun
equal to the old one. Useful to fix
definitional equalities.
Instances For
Copy of a CuspForm
with a new toFun
equal to the old one. Useful to fix
definitional equalities.
Instances For
Additive coercion from ModularForm
to ℍ → ℂ
.
Instances For
The modular form of weight k_1 + k_2
given by the product of two modular forms of weights
k_1
and k_2
.
Instances For
Additive coercion from CuspForm
to ℍ → ℂ
.