Documentation

Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Dimension formula and Sturm bound for level 1 modular forms #

This file proves the dimension formula and the Sturm bound for the space of modular forms for š’®ā„’ (= SL(2, ā„¤)) of even weight.

Main results #

source
noncomputable def CuspForm.ofMulDiscriminant {k : ā„¤} (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ā„).range (k - 12)) :
CuspForm (Matrix.SpecialLinearGroup.mapGL ā„).range k

Multiply a modular form of weight k - 12 by the discriminant to get a cusp form of weight k. Built directly as a CuspForm via CuspForm.mulModularForm.

Equations
Instances For
    source
    @[simp]
    theorem CuspForm.ofMulDiscriminant_apply {k : ā„¤} (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ā„).range (k - 12)) (z : UpperHalfPlane) :
    (ofMulDiscriminant f) z = ModularForm.discriminant z * f z
    source
    theorem CuspForm.divByDiscriminant_slash_eq {k : ā„¤} (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ā„).range k) (Ī³ : Matrix.SpecialLinearGroup (Fin 2) ā„¤) :
    (SlashAction.map (k - 12) Ī³ fun (z : UpperHalfPlane) => f z / ModularForm.discriminant z) = fun (z : UpperHalfPlane) => f z / ModularForm.discriminant z
    source
    noncomputable def CuspForm.discriminantEquiv {k : ā„¤} :
    CuspForm (Matrix.SpecialLinearGroup.mapGL ā„).range k ā‰ƒā‚—[ā„‚] ModularForm (Matrix.SpecialLinearGroup.mapGL ā„).range (k - 12)

    The linear equivalence between cusp forms of weight k and modular forms of weight k - 12, given by division by the discriminant.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem CuspForm.discriminantEquiv_apply {k : ā„¤} (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ā„).range k) (z : UpperHalfPlane) :
      (discriminantEquiv f) z = f z / ModularForm.discriminant z
      source
      @[deprecated CuspForm.discriminantEquiv (since := "2026-05-18")]
      noncomputable def CuspForm.divDiscriminant {k : ā„¤} (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ā„).range k) :
      ModularForm (Matrix.SpecialLinearGroup.mapGL ā„).range (k - 12)

      Divide a cusp form by the discriminant to get a modular form of weight k - 12.

      Equations
      Instances For
        source
        @[deprecated CuspForm.discriminantEquiv_apply (since := "2026-05-18")]
        theorem CuspForm.divDiscriminant_apply {k : ā„¤} (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ā„).range k) (z : UpperHalfPlane) :
        f.divDiscriminant z = f z / ModularForm.discriminant z
        source
        @[simp]
        theorem ModularForm.discriminant_mul_discriminantEquiv_apply {k : ā„¤} (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ā„).range k) (z : UpperHalfPlane) :
        discriminant z * (CuspForm.discriminantEquiv f) z = f z
        source
        @[simp]
        theorem ModularForm.discriminant_mul_discriminantEquiv {k : ā„¤} (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ā„).range k) :
        discriminant * ā‡‘(CuspForm.discriminantEquiv f) = ā‡‘f
        source
        theorem ModularForm.discriminant_qExpansion_order :
        (UpperHalfPlane.qExpansion 1 discriminant).order = 1

        The order of the q-expansion of the modular discriminant is 1: the zeroth coefficient vanishes (Ī” is a cusp form) and the first coefficient equals 1.

        source
        theorem ModularForm.qExpansion_eq_qExpansion_discriminant_mul {k : ā„¤} (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ā„).range k) (hcusp : (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 ā‡‘f) = 0) :
        UpperHalfPlane.qExpansion 1 ā‡‘f = UpperHalfPlane.qExpansion 1 discriminant * UpperHalfPlane.qExpansion 1 ā‡‘(CuspForm.discriminantEquiv (f.toCuspForm hcusp))

        The q-expansion of a level-1 modular form whose zeroth coefficient vanishes factors as the q-expansion of Ī” times the q-expansion of the corresponding form of weight k - 12 obtained via discriminantEquiv.

        source
        theorem ModularForm.levelOne_odd_weight_eq_zero {k : ā„¤} (hk : Odd k) (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ā„).range k) :
        f = 0

        A š’®ā„’ modular form of odd weight is zero (evaluate at -1 āˆˆ SL(2, ā„¤)).

        source
        theorem ModularForm.levelOne_odd_weight_rank_zero {k : ā„¤} (hk : Odd k) :
        Module.rank ā„‚ (ModularForm (Matrix.SpecialLinearGroup.mapGL ā„).range k) = 0

        Modular forms of odd weight for š’®ā„’ are zero-dimensional.

        source
        theorem CuspForm.rank_eq_zero_of_weight_lt_twelve {k : ā„¤} (hk : k < 12) :
        Module.rank ā„‚ (CuspForm (Matrix.SpecialLinearGroup.mapGL ā„).range k) = 0

        Cusp forms of weight k < 12 for š’®ā„’ are zero-dimensional.

        source
        theorem CuspForm.rank_eq_one_of_weight_eq_twelve :
        Module.rank ā„‚ (CuspForm (Matrix.SpecialLinearGroup.mapGL ā„).range 12) = 1

        The space of weight 12 cusp forms for š’®ā„’ has rank 1.

        source
        theorem CuspForm.exists_smul_discriminant_of_weight_eq_twelve (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ā„).range 12) :
        āˆƒ (c : ā„‚), c ā€¢ discriminant = f

        Every weight 12 cusp form for š’®ā„’ is a scalar multiple of the discriminant.

        source
        theorem ModularForm.rank_eq_one_add_rank_cuspForm {k : ā„•} (hk : 3 ā‰¤ k) (hk2 : Even k) :
        Module.rank ā„‚ (ModularForm (Matrix.SpecialLinearGroup.mapGL ā„).range ā†‘k) = 1 + Module.rank ā„‚ (CuspForm (Matrix.SpecialLinearGroup.mapGL ā„).range ā†‘k)

        For even k ā‰„ 3, the rank of š’®ā„’ modular forms is one more than the rank of cusp forms.

        source
        theorem ModularForm.levelOne_weight_four_rank_one :
        Module.rank ā„‚ (ModularForm (Matrix.SpecialLinearGroup.mapGL ā„).range 4) = 1
        source
        theorem ModularForm.levelOne_weight_six_rank_one :
        Module.rank ā„‚ (ModularForm (Matrix.SpecialLinearGroup.mapGL ā„).range 6) = 1
        source
        theorem ModularForm.Eā‚„_qExpansion_coeff_one :
        (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ā‡‘Eā‚„) = 240
        source
        theorem ModularForm.Eā‚†_qExpansion_coeff_one :
        (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ā‡‘Eā‚†) = -504
        source
        theorem ModularForm.levelOne_weight_two_rank_zero :
        Module.rank ā„‚ (ModularForm (Matrix.SpecialLinearGroup.mapGL ā„).range 2) = 0

        Modular forms of weight 2 for š’®ā„’ are zero.

        source
        theorem ModularForm.dimension_level_one (k : ā„•) (hk2 : Even k) :
        Module.rank ā„‚ (ModularForm (Matrix.SpecialLinearGroup.mapGL ā„).range ā†‘k) = ā†‘(if k ā‰” 2 [MOD 12] then k / 12 else k / 12 + 1)

        The dimension formula for š’®ā„’ modular forms of even weight.

        source
        instance ModularForm.instFiniteDimensionalComplexRangeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGL (k : ā„¤) :
        FiniteDimensional ā„‚ (ModularForm (Matrix.SpecialLinearGroup.mapGL ā„).range k)
        source
        theorem ModularForm.sturm_bound_levelOne_nat {k : ā„•} {f : ModularForm (Matrix.SpecialLinearGroup.mapGL ā„).range ā†‘k} (h : ā†‘(k / 12) < (UpperHalfPlane.qExpansion 1 ā‡‘f).order) :
        f = 0

        Sturm bound for level-1 modular forms (natural weight). If a modular form f of weight k : ā„• has q-expansion of order strictly greater than k / 12, then f is identically zero.

        source
        theorem ModularForm.sturm_bound_levelOne {k : ā„¤} {f : ModularForm (Matrix.SpecialLinearGroup.mapGL ā„).range k} (h : ā†‘(k.toNat / 12) < (UpperHalfPlane.qExpansion 1 ā‡‘f).order) :
        f = 0

        Sturm bound for level-1 modular forms. If a modular form f of weight k for SL(2, ā„¤) has q-expansion of order strictly greater than k / 12, then f is identically zero. Corollary of the natural-weight version sturm_bound_levelOne_nat.