Documentation

Mathlib.NumberTheory.ModularForms.Basic

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 SlashInvariantForms then we define the space of modular forms, cusp forms and prove that the product of two modular forms is a modular form.

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

Instances For

    These are SlashInvariantForms that are holomophic and zero at infinity.

    Instances For

      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

        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
          theorem ModularForm.toFun_eq_coe {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } (f : ModularForm Γ k) :
          f.toFun = f
          @[simp]
          theorem ModularForm.toSlashInvariantForm_coe {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } (f : ModularForm Γ k) :
          f.toSlashInvariantForm = f
          theorem CuspForm.toFun_eq_coe {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } {f : CuspForm Γ k} :
          f.toFun = f
          @[simp]
          theorem CuspForm.toSlashInvariantForm_coe {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } (f : CuspForm Γ k) :
          f.toSlashInvariantForm = f
          theorem ModularForm.ext {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } {f : ModularForm Γ k} {g : ModularForm Γ k} (h : ∀ (x : UpperHalfPlane), f x = g x) :
          f = g
          theorem CuspForm.ext {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } {f : CuspForm Γ k} {g : CuspForm Γ k} (h : ∀ (x : UpperHalfPlane), f x = g x) :
          f = g
          def ModularForm.copy {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } (f : ModularForm Γ k) (f' : UpperHalfPlane) (h : f' = f) :

          Copy of a ModularForm with a new toFun equal to the old one. Useful to fix definitional equalities.

          Instances For
            def CuspForm.copy {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } (f : CuspForm Γ k) (f' : UpperHalfPlane) (h : f' = f) :

            Copy of a CuspForm with a new toFun equal to the old one. Useful to fix definitional equalities.

            Instances For
              @[simp]
              theorem ModularForm.coe_add {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } (f : ModularForm Γ k) (g : ModularForm Γ k) :
              ↑(f + g) = f + g
              @[simp]
              theorem ModularForm.add_apply {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } (f : ModularForm Γ k) (g : ModularForm Γ k) (z : UpperHalfPlane) :
              ↑(f + g) z = f z + g z
              @[simp]
              @[simp]
              @[simp]
              theorem ModularForm.coe_smul {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } {α : Type u_2} [SMul α ] [IsScalarTower α ] (f : ModularForm Γ k) (n : α) :
              ↑(n f) = n f
              @[simp]
              theorem ModularForm.smul_apply {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } {α : Type u_2} [SMul α ] [IsScalarTower α ] (f : ModularForm Γ k) (n : α) (z : UpperHalfPlane) :
              ↑(n f) z = n f z
              @[simp]
              theorem ModularForm.coe_neg {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } (f : ModularForm Γ k) :
              ↑(-f) = -f
              @[simp]
              theorem ModularForm.neg_apply {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } (f : ModularForm Γ k) (z : UpperHalfPlane) :
              ↑(-f) z = -f z
              @[simp]
              theorem ModularForm.coe_sub {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } (f : ModularForm Γ k) (g : ModularForm Γ k) :
              ↑(f - g) = f - g
              @[simp]
              theorem ModularForm.sub_apply {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } (f : ModularForm Γ k) (g : ModularForm Γ k) (z : UpperHalfPlane) :
              ↑(f - g) z = f z - g z
              @[simp]
              theorem ModularForm.coeHom_apply {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } (f : ModularForm Γ k) (a : UpperHalfPlane) :
              ModularForm.coeHom f a = f a

              Additive coercion from ModularForm to ℍ → ℂ.

              Instances For
                def ModularForm.mul {k_1 : } {k_2 : } {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} (f : ModularForm Γ k_1) (g : ModularForm Γ k_2) :
                ModularForm Γ (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.

                Instances For
                  @[simp]
                  theorem ModularForm.mul_coe {k_1 : } {k_2 : } {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} (f : ModularForm Γ k_1) (g : ModularForm Γ k_2) :
                  ↑(ModularForm.mul f g) = f * g
                  @[simp]
                  theorem CuspForm.coe_add {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } (f : CuspForm Γ k) (g : CuspForm Γ k) :
                  ↑(f + g) = f + g
                  @[simp]
                  theorem CuspForm.add_apply {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } (f : CuspForm Γ k) (g : CuspForm Γ k) (z : UpperHalfPlane) :
                  ↑(f + g) z = f z + g z
                  @[simp]
                  theorem CuspForm.coe_zero {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } :
                  0 = 0
                  @[simp]
                  instance CuspForm.instSMul {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } {α : Type u_2} [SMul α ] [IsScalarTower α ] :
                  SMul α (CuspForm Γ k)
                  @[simp]
                  theorem CuspForm.coe_smul {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } {α : Type u_2} [SMul α ] [IsScalarTower α ] (f : CuspForm Γ k) (n : α) :
                  ↑(n f) = n f
                  @[simp]
                  theorem CuspForm.smul_apply {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } {α : Type u_2} [SMul α ] [IsScalarTower α ] (f : CuspForm Γ k) (n : α) {z : UpperHalfPlane} :
                  ↑(n f) z = n f z
                  @[simp]
                  theorem CuspForm.coe_neg {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } (f : CuspForm Γ k) :
                  ↑(-f) = -f
                  @[simp]
                  theorem CuspForm.neg_apply {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } (f : CuspForm Γ k) (z : UpperHalfPlane) :
                  ↑(-f) z = -f z
                  @[simp]
                  theorem CuspForm.coe_sub {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } (f : CuspForm Γ k) (g : CuspForm Γ k) :
                  ↑(f - g) = f - g
                  @[simp]
                  theorem CuspForm.sub_apply {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } (f : CuspForm Γ k) (g : CuspForm Γ k) (z : UpperHalfPlane) :
                  ↑(f - g) z = f z - g z
                  @[simp]
                  theorem CuspForm.coeHom_apply {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } (f : CuspForm Γ k) (a : UpperHalfPlane) :
                  CuspForm.coeHom f a = f a

                  Additive coercion from CuspForm to ℍ → ℂ.

                  Instances For