Theorems · Theorem · number theory

ModularForm.sturm_bound_levelOne

∀ {k : ℤ} {f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k},
  ↑(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.

Defined in

Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Cited by

0 results in Mathlib

Foundations

Depth 337 from the axioms · uses propext, Classical.choice, Quot.sound