mathlib3documentation

number_theory.modular_forms.basic

Modular forms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines modular forms and proves some basic properties about them.

We begin by defining modular forms and cusp forms as extension of slash_invariant_forms then we define the space of modular forms, cusp forms and prove that the product of two modular forms is a modular form.

structure modular_form (Γ : subgroup ) (k : ) :

These are slash_invariant_form's that are holomophic and bounded at infinity.

Instances for modular_form
def modular_form.to_slash_invariant_form {Γ : subgroup } {k : } (self : k) :

The slash_invariant_form associated to a modular_form.

def cusp_form.to_slash_invariant_form {Γ : subgroup } {k : } (self : k) :

The slash_invariant_form associated to a cusp_form.

structure cusp_form (Γ : subgroup ) (k : ) :

These are slash_invariant_forms that are holomophic and zero at infinity.

Instances for cusp_form
@[instance]
def modular_form_class.to_slash_invariant_form_class (F : Type u_1) (Γ : subgroup ) (k : ) [self : k] :
@[class]
structure modular_form_class (F : Type u_1) (Γ : subgroup ) (k : ) :
Type u_1

modular_form_class F Γ k says that F is a type of bundled functions that extend slash_invariant_form_class by requiring that the functions be holomorphic and bounded at infinity.

Instances of this typeclass
Instances of other typeclasses for modular_form_class
• modular_form_class.has_sizeof_inst
@[instance]
def cusp_form_class.to_slash_invariant_form_class (F : Type u_1) (Γ : subgroup ) (k : ) [self : k] :
@[class]
structure cusp_form_class (F : Type u_1) (Γ : subgroup ) (k : ) :
Type u_1

cusp_form_class F Γ k says that F is a type of bundled functions that extend slash_invariant_form_class by requiring that the functions be holomorphic and zero at infinity.

Instances of this typeclass
Instances of other typeclasses for cusp_form_class
• cusp_form_class.has_sizeof_inst
@[protected, instance]
def modular_form_class.modular_form (Γ : subgroup ) (k : ) :
Γ k
Equations
@[protected, instance]
def cusp_form_class.cusp_form (Γ : subgroup ) (k : ) :
Equations
@[simp]
theorem modular_form_to_fun_eq_coe {Γ : subgroup } {k : } {f : k} :
@[simp]
theorem cusp_form_to_fun_eq_coe {Γ : subgroup } {k : } {f : k} :
@[ext]
theorem modular_form.ext {Γ : subgroup } {k : } {f g : k} (h : (x : upper_half_plane), f x = g x) :
f = g
@[ext]
theorem cusp_form.ext {Γ : subgroup } {k : } {f g : k} (h : (x : upper_half_plane), f x = g x) :
f = g
@[protected]
def modular_form.copy {Γ : subgroup } {k : } (f : k) (f' : upper_half_plane ) (h : f' = f) :
k

Copy of a modular_form with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
@[protected]
def cusp_form.copy {Γ : subgroup } {k : } (f : k) (f' : upper_half_plane ) (h : f' = f) :
k

Copy of a cusp_form with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
@[protected, instance]
def modular_form.has_add {Γ : subgroup } {k : } :
Equations
@[simp]
theorem modular_form.coe_add {Γ : subgroup } {k : } (f g : k) :
(f + g) = f + g
@[simp]
theorem modular_form.add_apply {Γ : subgroup } {k : } (f g : k) (z : upper_half_plane) :
(f + g) z = f z + g z
@[protected, instance]
def modular_form.has_zero {Γ : subgroup } {k : } :
Equations
@[simp]
theorem modular_form.coe_zero {Γ : subgroup } {k : } :
0 = 0
@[simp]
theorem modular_form.zero_apply {Γ : subgroup } {k : } (z : upper_half_plane) :
0 z = 0
@[protected, instance]
def modular_form.has_smul {Γ : subgroup } {k : } {α : Type u_2} [ ] [ ] :
k)
Equations
@[simp]
theorem modular_form.coe_smul {Γ : subgroup } {k : } {α : Type u_2} [ ] [ ] (f : k) (n : α) :
(n f) = n f
@[simp]
theorem modular_form.smul_apply {Γ : subgroup } {k : } {α : Type u_2} [ ] [ ] (f : k) (n : α) (z : upper_half_plane) :
(n f) z = n f z
@[protected, instance]
def modular_form.has_neg {Γ : subgroup } {k : } :
Equations
@[simp]
theorem modular_form.coe_neg {Γ : subgroup } {k : } (f : k) :
@[simp]
theorem modular_form.neg_apply {Γ : subgroup } {k : } (f : k) (z : upper_half_plane) :
(-f) z = -f z
@[protected, instance]
def modular_form.has_sub {Γ : subgroup } {k : } :
Equations
@[simp]
theorem modular_form.coe_sub {Γ : subgroup } {k : } (f g : k) :
(f - g) = f - g
@[simp]
theorem modular_form.sub_apply {Γ : subgroup } {k : } (f g : k) (z : upper_half_plane) :
(f - g) z = f z - g z
@[protected, instance]
Equations
def modular_form.coe_hom {Γ : subgroup } {k : } :

Additive coercion from modular_form to ℍ → ℂ.

Equations
@[simp]
theorem modular_form.coe_hom_apply {Γ : subgroup } {k : } (f : k) (ᾰ : upper_half_plane) :
= f ᾰ
@[protected, instance]
noncomputable def modular_form.module {Γ : subgroup } {k : } :
k)
Equations
@[protected, instance]
def modular_form.inhabited {Γ : subgroup } {k : } :
Equations
def modular_form.mul {k_1 k_2 : } {Γ : subgroup } (f : k_1) (g : k_2) :
(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.

Equations
@[simp]
theorem modular_form.mul_coe {k_1 k_2 : } {Γ : subgroup } (f : k_1) (g : k_2) :
(f.mul g) = f * g
@[protected, instance]
Equations
@[simp]
theorem modular_form.one_coe_eq_one {Γ : subgroup } :
1 = 1
@[protected, instance]
def cusp_form.has_add {Γ : subgroup } {k : } :
Equations
@[simp]
theorem cusp_form.coe_add {Γ : subgroup } {k : } (f g : k) :
(f + g) = f + g
@[simp]
theorem cusp_form.add_apply {Γ : subgroup } {k : } (f g : k) (z : upper_half_plane) :
(f + g) z = f z + g z
@[protected, instance]
def cusp_form.has_zero {Γ : subgroup } {k : } :
Equations
@[simp]
theorem cusp_form.coe_zero {Γ : subgroup } {k : } :
0 = 0
@[simp]
theorem cusp_form.zero_apply {Γ : subgroup } {k : } (z : upper_half_plane) :
0 z = 0
@[protected, instance]
def cusp_form.has_smul {Γ : subgroup } {k : } {α : Type u_2} [ ] [ ] :
k)
Equations
@[simp]
theorem cusp_form.coe_smul {Γ : subgroup } {k : } {α : Type u_2} [ ] [ ] (f : k) (n : α) :
(n f) = n f
@[simp]
theorem cusp_form.smul_apply {Γ : subgroup } {k : } {α : Type u_2} [ ] [ ] (f : k) (n : α) {z : upper_half_plane} :
(n f) z = n f z
@[protected, instance]
def cusp_form.has_neg {Γ : subgroup } {k : } :
Equations
@[simp]
theorem cusp_form.coe_neg {Γ : subgroup } {k : } (f : k) :
@[simp]
theorem cusp_form.neg_apply {Γ : subgroup } {k : } (f : k) (z : upper_half_plane) :
(-f) z = -f z
@[protected, instance]
def cusp_form.has_sub {Γ : subgroup } {k : } :
Equations
@[simp]
theorem cusp_form.coe_sub {Γ : subgroup } {k : } (f g : k) :
(f - g) = f - g
@[simp]
theorem cusp_form.sub_apply {Γ : subgroup } {k : } (f g : k) (z : upper_half_plane) :
(f - g) z = f z - g z
@[protected, instance]
Equations
@[simp]
theorem cusp_form.coe_hom_apply {Γ : subgroup } {k : } (f : k) (ᾰ : upper_half_plane) :
= f ᾰ
def cusp_form.coe_hom {Γ : subgroup } {k : } :

Additive coercion from cusp_form to ℍ → ℂ.

Equations
@[protected, instance]
noncomputable def cusp_form.module {Γ : subgroup } {k : } :
k)
Equations
@[protected, instance]
def cusp_form.inhabited {Γ : subgroup } {k : } :
Equations
@[protected, instance]
def cusp_form.modular_form_class {F : Type u_1} {Γ : subgroup } {k : } [ k] :
k
Equations