number_theory.modular_forms.basic

structure modular_form (Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)) (k : ℤ) :

to_fun : upper_half_plane → ℂ
slash_action_eq' : ∀ (γ : ↥Γ), slash_action.map ℂ k γ self.to_fun = self.to_fun
holo' : mdifferentiable (model_with_corners_self ℂ ℂ) (model_with_corners_self ℂ ℂ) self.to_fun
bdd_at_infty' : ∀ (A : matrix.special_linear_group (fin 2) ℤ), upper_half_plane.is_bounded_at_im_infty (slash_action.map ℂ k A self.to_fun)

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 (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} (self : modular_form Γ k) :

slash_invariant_form Γ k

The slash_invariant_form associated to a modular_form.

source

def cusp_form.to_slash_invariant_form {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} (self : cusp_form Γ k) :

slash_invariant_form Γ k

The slash_invariant_form associated to a cusp_form.

source

structure cusp_form (Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)) (k : ℤ) :

Type

to_fun : upper_half_plane → ℂ
slash_action_eq' : ∀ (γ : ↥Γ), slash_action.map ℂ k γ self.to_fun = self.to_fun
holo' : mdifferentiable (model_with_corners_self ℂ ℂ) (model_with_corners_self ℂ ℂ) self.to_fun
zero_at_infty' : ∀ (A : matrix.special_linear_group (fin 2) ℤ), upper_half_plane.is_zero_at_im_infty (slash_action.map ℂ k A self.to_fun)

These are slash_invariant_forms that are holomophic and zero at infinity.

Instances for cusp_form

source

@[instance]

def modular_form_class.to_slash_invariant_form_class (F : Type u_1) (Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)) (k : ℤ) [self : modular_form_class F Γ k] :

slash_invariant_form_class F Γ k

source

@[class]

structure modular_form_class (F : Type u_1) (Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)) (k : ℤ) :

Type u_1

coe : F → Π (a : upper_half_plane), (λ (_x : upper_half_plane), ℂ) a
coe_injective' : function.injective (modular_form_class.coe Γ k)
slash_action_eq : ∀ (f : F) (γ : ↥Γ), slash_action.map ℂ k γ ⇑f = ⇑f
holo : ∀ (f : F), mdifferentiable (model_with_corners_self ℂ ℂ) (model_with_corners_self ℂ ℂ) ⇑f
bdd_at_infty : ∀ (f : F) (A : matrix.special_linear_group (fin 2) ℤ), upper_half_plane.is_bounded_at_im_infty (slash_action.map ℂ k A ⇑f)

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

source

@[instance]

def cusp_form_class.to_slash_invariant_form_class (F : Type u_1) (Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)) (k : ℤ) [self : cusp_form_class F Γ k] :

slash_invariant_form_class F Γ k

source

@[class]

structure cusp_form_class (F : Type u_1) (Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)) (k : ℤ) :

Type u_1

coe : F → Π (a : upper_half_plane), (λ (_x : upper_half_plane), ℂ) a
coe_injective' : function.injective (cusp_form_class.coe Γ k)
slash_action_eq : ∀ (f : F) (γ : ↥Γ), slash_action.map ℂ k γ ⇑f = ⇑f
holo : ∀ (f : F), mdifferentiable (model_with_corners_self ℂ ℂ) (model_with_corners_self ℂ ℂ) ⇑f
zero_at_infty : ∀ (f : F) (A : matrix.special_linear_group (fin 2) ℤ), upper_half_plane.is_zero_at_im_infty (slash_action.map ℂ k A ⇑f)

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

cusp_form_class.cusp_form

Instances of other typeclasses for cusp_form_class

cusp_form_class.has_sizeof_inst

source

@[protected, instance]

def modular_form_class.modular_form (Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)) (k : ℤ) :

modular_form_class (modular_form Γ k) Γ k

Equations

modular_form_class.modular_form Γ k = {coe := modular_form.to_fun k, coe_injective' := _, slash_action_eq := _, holo := _, bdd_at_infty := _}

source

@[protected, instance]

def cusp_form_class.cusp_form (Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)) (k : ℤ) :

cusp_form_class (cusp_form Γ k) Γ k

Equations

cusp_form_class.cusp_form Γ k = {coe := cusp_form.to_fun k, coe_injective' := _, slash_action_eq := _, holo := _, zero_at_infty := _}

source

@[simp]

theorem modular_form_to_fun_eq_coe {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} {f : modular_form Γ k} :

f.to_fun = ⇑f

source

@[simp]

theorem cusp_form_to_fun_eq_coe {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} {f : cusp_form Γ k} :

f.to_fun = ⇑f

source

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

source

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

source

@[protected]

def modular_form.copy {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} (f : modular_form Γ k) (f' : upper_half_plane → ℂ) (h : f' = ⇑f) :

modular_form Γ k

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

Equations

f.copy f' h = {to_fun := f', slash_action_eq' := _, holo' := _, bdd_at_infty' := _}

source

@[protected]

def cusp_form.copy {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} (f : cusp_form Γ k) (f' : upper_half_plane → ℂ) (h : f' = ⇑f) :

cusp_form Γ k

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

Equations

f.copy f' h = {to_fun := f', slash_action_eq' := _, holo' := _, zero_at_infty' := _}

source

@[protected, instance]

def modular_form.has_add {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} :

has_add (modular_form Γ k)

Equations

modular_form.has_add = {add := λ (f g : modular_form Γ k), {to_fun := (↑f + ↑g).to_fun, slash_action_eq' := _, holo' := _, bdd_at_infty' := _}}

source

@[simp]

theorem modular_form.coe_add {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} (f g : modular_form Γ k) :

⇑(f + g) = ⇑f + ⇑g

source

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

source

@[protected, instance]

def modular_form.has_zero {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} :

has_zero (modular_form Γ k)

Equations

modular_form.has_zero = {zero := {to_fun := 0.to_fun, slash_action_eq' := _, holo' := _, bdd_at_infty' := _}}

source

@[simp]

theorem modular_form.coe_zero {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} :

⇑0 = 0

source

@[simp]

theorem modular_form.zero_apply {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} (z : upper_half_plane) :

⇑0 z = 0

source

@[protected, instance]

def modular_form.has_smul {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} {α : Type u_2} [has_smul α ℂ] [is_scalar_tower α ℂ ℂ] :

has_smul α (modular_form Γ k)

Equations

modular_form.has_smul = {smul := λ (c : α) (f : modular_form Γ k), {to_fun := c • ⇑f, slash_action_eq' := _, holo' := _, bdd_at_infty' := _}}

source

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

source

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

source

@[protected, instance]

def modular_form.has_neg {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} :

has_neg (modular_form Γ k)

Equations

modular_form.has_neg = {neg := λ (f : modular_form Γ k), {to_fun := -⇑f, slash_action_eq' := _, holo' := _, bdd_at_infty' := _}}

source

@[simp]

theorem modular_form.coe_neg {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} (f : modular_form Γ k) :

⇑-f = -⇑f

source

@[simp]

theorem modular_form.neg_apply {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} (f : modular_form Γ k) (z : upper_half_plane) :

(⇑-f) z = -⇑f z

source

@[protected, instance]

def modular_form.has_sub {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} :

has_sub (modular_form Γ k)

Equations

modular_form.has_sub = {sub := λ (f g : modular_form Γ k), f + -g}

source

@[simp]

theorem modular_form.coe_sub {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} (f g : modular_form Γ k) :

⇑(f - g) = ⇑f - ⇑g

source

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

source

@[protected, instance]

def modular_form.add_comm_group {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} :

add_comm_group (modular_form Γ k)

Equations

modular_form.add_comm_group = function.injective.add_comm_group coe_fn modular_form.add_comm_group._proof_3 modular_form.add_comm_group._proof_4 modular_form.coe_add modular_form.coe_neg modular_form.coe_sub modular_form.add_comm_group._proof_5 modular_form.add_comm_group._proof_6

source

def modular_form.coe_hom {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} :

modular_form Γ k →+ upper_half_plane → ℂ

Additive coercion from modular_form to ℍ → ℂ.

Equations

modular_form.coe_hom = {to_fun := λ (f : modular_form Γ k), ⇑f, map_zero' := _, map_add' := _}

source

@[simp]

theorem modular_form.coe_hom_apply {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} (f : modular_form Γ k) (ᾰ : upper_half_plane) :

⇑modular_form.coe_hom f ᾰ = ⇑f ᾰ

source

@[protected, instance]

noncomputable def modular_form.module {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} :

module ℂ (modular_form Γ k)

Equations

modular_form.module = function.injective.module ℂ modular_form.coe_hom modular_form.module._proof_2 modular_form.module._proof_3

source

@[protected, instance]

def modular_form.inhabited {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} :

inhabited (modular_form Γ k)

Equations

modular_form.inhabited = {default := 0}

source

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

f.mul g = {to_fun := ⇑f * ⇑g, slash_action_eq' := _, holo' := _, bdd_at_infty' := _}

source

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

source

@[protected, instance]

def modular_form.has_one {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} :

has_one (modular_form Γ 0)

Equations

modular_form.has_one = {one := {to_fun := 1.to_fun, slash_action_eq' := _, holo' := _, bdd_at_infty' := _}}

source

@[simp]

theorem modular_form.one_coe_eq_one {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} :

⇑1 = 1

source

@[protected, instance]

def cusp_form.has_add {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} :

has_add (cusp_form Γ k)

Equations

cusp_form.has_add = {add := λ (f g : cusp_form Γ k), {to_fun := ⇑f + ⇑g, slash_action_eq' := _, holo' := _, zero_at_infty' := _}}

source

@[simp]

theorem cusp_form.coe_add {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} (f g : cusp_form Γ k) :

⇑(f + g) = ⇑f + ⇑g

source

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

source

@[protected, instance]

def cusp_form.has_zero {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} :

has_zero (cusp_form Γ k)

Equations

cusp_form.has_zero = {zero := {to_fun := 0, slash_action_eq' := _, holo' := cusp_form.has_zero._proof_2, zero_at_infty' := _}}

source

@[simp]

theorem cusp_form.coe_zero {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} :

⇑0 = 0

source

@[simp]

theorem cusp_form.zero_apply {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} (z : upper_half_plane) :

⇑0 z = 0

source

@[protected, instance]

def cusp_form.has_smul {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} {α : Type u_2} [has_smul α ℂ] [is_scalar_tower α ℂ ℂ] :

has_smul α (cusp_form Γ k)

Equations

cusp_form.has_smul = {smul := λ (c : α) (f : cusp_form Γ k), {to_fun := c • ⇑f, slash_action_eq' := _, holo' := _, zero_at_infty' := _}}

source

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

source

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

source

@[protected, instance]

def cusp_form.has_neg {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} :

has_neg (cusp_form Γ k)

Equations

cusp_form.has_neg = {neg := λ (f : cusp_form Γ k), {to_fun := -⇑f, slash_action_eq' := _, holo' := _, zero_at_infty' := _}}

source

@[simp]

theorem cusp_form.coe_neg {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} (f : cusp_form Γ k) :

⇑-f = -⇑f

source

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

source

@[protected, instance]

def cusp_form.has_sub {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} :

has_sub (cusp_form Γ k)

Equations

cusp_form.has_sub = {sub := λ (f g : cusp_form Γ k), f + -g}

source

@[simp]

theorem cusp_form.coe_sub {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} (f g : cusp_form Γ k) :

⇑(f - g) = ⇑f - ⇑g

source

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

source

@[protected, instance]

def cusp_form.add_comm_group {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} :

add_comm_group (cusp_form Γ k)

Equations

cusp_form.add_comm_group = function.injective.add_comm_group coe_fn cusp_form.add_comm_group._proof_3 cusp_form.add_comm_group._proof_4 cusp_form.coe_add cusp_form.coe_neg cusp_form.coe_sub cusp_form.add_comm_group._proof_5 cusp_form.add_comm_group._proof_6

source

@[simp]

theorem cusp_form.coe_hom_apply {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} (f : cusp_form Γ k) (ᾰ : upper_half_plane) :

⇑cusp_form.coe_hom f ᾰ = ⇑f ᾰ

source

def cusp_form.coe_hom {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} :

cusp_form Γ k →+ upper_half_plane → ℂ

Additive coercion from cusp_form to ℍ → ℂ.

Equations

cusp_form.coe_hom = {to_fun := λ (f : cusp_form Γ k), ⇑f, map_zero' := _, map_add' := _}

source

@[protected, instance]

noncomputable def cusp_form.module {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} :

module ℂ (cusp_form Γ k)

Equations

cusp_form.module = function.injective.module ℂ cusp_form.coe_hom cusp_form.module._proof_2 cusp_form.module._proof_3

source

@[protected, instance]

def cusp_form.inhabited {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} :

inhabited (cusp_form Γ k)

Equations

cusp_form.inhabited = {default := 0}

source

@[protected, instance]

def cusp_form.modular_form_class {F : Type u_1} {Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)} {k : ℤ} [cusp_form_class F Γ k] :

modular_form_class F Γ k

Equations

cusp_form.modular_form_class = {coe := fun_like.coe (slash_invariant_form_class.to_fun_like F Γ k), coe_injective' := _, slash_action_eq := _, holo := _, bdd_at_infty := _}

mathlib3 documentation

Modular forms #