mathlib3 documentation

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.

@[class]
structure modular_form_class (F : Type u_1) (Γ : subgroup (matrix.special_linear_group (fin 2) )) (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
@[class]
structure cusp_form_class (F : Type u_1) (Γ : subgroup (matrix.special_linear_group (fin 2) )) (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
@[simp]
@[ext]
theorem modular_form.ext {Γ : subgroup (matrix.special_linear_group (fin 2) )} {k : } {f g : modular_form Γ k} (h : (x : upper_half_plane), f x = g x) :
f = g
@[ext]
theorem cusp_form.ext {Γ : subgroup (matrix.special_linear_group (fin 2) )} {k : } {f g : cusp_form Γ k} (h : (x : upper_half_plane), f x = g x) :
f = g
@[protected]

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 (matrix.special_linear_group (fin 2) )} {k : } (f : cusp_form Γ k) (f' : upper_half_plane ) (h : f' = f) :

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

Equations
@[protected, instance]
Equations
@[simp]
theorem modular_form.coe_add {Γ : subgroup (matrix.special_linear_group (fin 2) )} {k : } (f g : modular_form Γ k) :
(f + g) = f + g
@[simp]
theorem modular_form.add_apply {Γ : subgroup (matrix.special_linear_group (fin 2) )} {k : } (f g : modular_form Γ k) (z : upper_half_plane) :
(f + g) z = f z + g z
@[protected, instance]
Equations
@[simp]
@[protected, instance]
Equations
@[simp]
theorem modular_form.coe_smul {Γ : subgroup (matrix.special_linear_group (fin 2) )} {k : } {α : Type u_2} [has_smul α ] [is_scalar_tower α ] (f : modular_form Γ k) (n : α) :
(n f) = n f
@[simp]
theorem modular_form.smul_apply {Γ : subgroup (matrix.special_linear_group (fin 2) )} {k : } {α : Type u_2} [has_smul α ] [is_scalar_tower α ] (f : modular_form Γ k) (n : α) (z : upper_half_plane) :
(n f) z = n f z
@[protected, instance]
Equations
@[simp]
@[simp]
@[protected, instance]
Equations
@[simp]
theorem modular_form.coe_sub {Γ : subgroup (matrix.special_linear_group (fin 2) )} {k : } (f g : modular_form Γ k) :
(f - g) = f - g
@[simp]
theorem modular_form.sub_apply {Γ : subgroup (matrix.special_linear_group (fin 2) )} {k : } (f g : modular_form Γ k) (z : upper_half_plane) :
(f - g) z = f z - g z
@[protected, instance]
Equations

Additive coercion from modular_form to ℍ → ℂ.

Equations
@[protected, instance]
noncomputable def modular_form.module {Γ : subgroup (matrix.special_linear_group (fin 2) )} {k : } :
Equations
@[protected, instance]
Equations
def modular_form.mul {k_1 k_2 : } {Γ : subgroup (matrix.special_linear_group (fin 2) )} (f : modular_form Γ k_1) (g : modular_form Γ k_2) :
modular_form Γ (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 (matrix.special_linear_group (fin 2) )} (f : modular_form Γ k_1) (g : modular_form Γ k_2) :
(f.mul g) = f * g
@[protected, instance]
Equations
@[simp]
theorem cusp_form.coe_add {Γ : subgroup (matrix.special_linear_group (fin 2) )} {k : } (f g : cusp_form Γ k) :
(f + g) = f + g
@[simp]
theorem cusp_form.add_apply {Γ : subgroup (matrix.special_linear_group (fin 2) )} {k : } (f g : cusp_form Γ k) (z : upper_half_plane) :
(f + g) z = f z + g z
@[protected, instance]
Equations
@[simp]
@[simp]
@[protected, instance]
Equations
@[simp]
theorem cusp_form.coe_smul {Γ : subgroup (matrix.special_linear_group (fin 2) )} {k : } {α : Type u_2} [has_smul α ] [is_scalar_tower α ] (f : cusp_form Γ k) (n : α) :
(n f) = n f
@[simp]
theorem cusp_form.smul_apply {Γ : subgroup (matrix.special_linear_group (fin 2) )} {k : } {α : Type u_2} [has_smul α ] [is_scalar_tower α ] (f : cusp_form Γ k) (n : α) {z : upper_half_plane} :
(n f) z = n f z
@[protected, instance]
Equations
@[simp]
theorem cusp_form.coe_neg {Γ : subgroup (matrix.special_linear_group (fin 2) )} {k : } (f : cusp_form Γ k) :
@[simp]
theorem cusp_form.neg_apply {Γ : subgroup (matrix.special_linear_group (fin 2) )} {k : } (f : cusp_form Γ k) (z : upper_half_plane) :
(-f) z = -f z
@[protected, instance]
Equations
@[simp]
theorem cusp_form.coe_sub {Γ : subgroup (matrix.special_linear_group (fin 2) )} {k : } (f g : cusp_form Γ k) :
(f - g) = f - g
@[simp]
theorem cusp_form.sub_apply {Γ : subgroup (matrix.special_linear_group (fin 2) )} {k : } (f g : cusp_form Γ k) (z : upper_half_plane) :
(f - g) z = f z - g z
@[protected, instance]
Equations

Additive coercion from cusp_form to ℍ → ℂ.

Equations
@[protected, instance]
noncomputable def cusp_form.module {Γ : subgroup (matrix.special_linear_group (fin 2) )} {k : } :
Equations
@[protected, instance]
Equations