A cusp-form dimension lower bound from weighted monomials

Proved

CuspForm.finrank_lower_bound_of_weighted_forms

by cbirkbeck · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

modular-formsnumber-theory

Let $\Gamma$ be a determinant-one subgroup with positive strict period $h$ . Suppose $A\in M_1(\Gamma)$ and $B\in M_d(\Gamma)$ have $h$ -q-expansion orders zero and one, respectively, and $D\in S_r(\Gamma)$ is nonzero. For integers $d>0$ and $k\ge r$ , if $S_k(\Gamma)$ is finite-dimensional, then

\left\lfloor\frac{k-r}{d}\right\rfloor+1\le\dim_{\mathbf C}S_k(\Gamma).

The independent cusp forms are $D A^{k-r-di}B^i$ , with $0\le i\le\lfloor(k-r)/d\rfloor$ . This is a shared input for the level-three and level-four MTT frontier dimension bounds.

Preamble

import Mathlib.NumberTheory.ModularForms.QExpansion
import Mathlib.LinearAlgebra.Dimension.Finite
open UpperHalfPlane
open scoped MatrixGroups

Formal statement

theorem CuspForm.finrank_lower_bound_of_weighted_forms
    {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] {d r k : ℕ} (hd : 0 < d) (hr : r ≤ k)
    (A : ModularForm Γ 1) (B : ModularForm Γ (d : ℤ)) (D : CuspForm Γ (r : ℤ))
    (h : ℝ) (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods)
    (hA : (qExpansion h A).order = 0) (hB : (qExpansion h B).order = 1) (hD : D ≠ 0)
    [FiniteDimensional ℂ (CuspForm Γ (k : ℤ))] :
    (k - r) / d + 1 ≤ Module.finrank ℂ (CuspForm Γ (k : ℤ)) := by sorry

Source

Direct weighted-monomial and q-expansion argument for MTT frontier theorems 74b9a146-622e-4d74-af58-7aa82330d5cb and 95cbc152-c054-48f1-a94f-c99cda423e6c. The proof is supplied in full; this statement does not assume a modular-form dimension formula.

View graph