Level-one cusp forms: odd-weight vanishing and the dimension formula

Mathlib's Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula proves that every level-one modular form of odd weight vanishes (ModularForm.levelOne_odd_weight_eq_zero), and computes the dimension of the space of level-one modular forms of even weight (ModularForm.dimension_level_one). This file records the CuspForm companions: the first via the injective inclusion CuspForm.toModularFormₗ, the second from the decomposition dim M_k = 1 + dim S_k (ModularForm.rank_eq_one_add_rank_cuspForm) in weight k ≥ 3.

Main results

• CuspForm.levelOne_odd_weight_eq_zero: every cusp form of odd weight on SL(2, ℤ) is zero.
• CuspForm.dimension_level_one: for even k, dim S_k(SL(2, ℤ)) is ⌊k / 12⌋ - 1 if k ≡ 2 (mod 12) and ⌊k / 12⌋ otherwise.

theorem CuspForm.levelOne_odd_weight_eq_zero {k : ℤ} (hk : Odd k) (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) : f = 0

A level-one cusp form of odd weight is zero, the CuspForm companion to ModularForm.levelOne_odd_weight_eq_zero.

theorem CuspForm.dimension_level_one (k : ℕ) (hk2 : Even k) : Module.finrank ℂ (CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) = if k ≡ 2 [MOD 12] then k / 12 - 1 else k / 12

The dimension formula for level-one cusp forms of even weight: dim S_k(SL(2, ℤ)) is ⌊k / 12⌋ - 1 if k ≡ 2 (mod 12) and ⌊k / 12⌋ otherwise. This is the CuspForm companion to ModularForm.dimension_level_one; in weights below 12 both sides vanish.