Documentation

TauCeti.NumberTheory.ModularForms.SturmBound

The Sturm bound for finite-index subgroups of SL(2, โ„ค) #

For ๐’ข โ‰ค GL(2, โ„) of finite relative index in ๐’ฎโ„’ with discrete strict periods and f : ModularForm ๐’ข k, if the q-expansion of f at the cusp โˆž (with cusp width ๐’ข.strictWidthInfty) has order strictly greater than k ยท [๐’ฎโ„’ : ๐’ข โŠ“ ๐’ฎโ„’] / 12, then f = 0.

The proof lifts the level-one bound ModularForm.sturm_bound_levelOne through the norm map: the norm of f vanishes exactly when f does, and by the decomposition TauCeti.ModularForm.qExpansion_one_norm_order_eq sufficient vanishing of f at โˆž propagates to the norm.

Main declarations #

References #

source
theorem TauCeti.ModularForm.sturm_bound_finiteIndex {๐’ข : Subgroup (GL (Fin 2) โ„)} [๐’ข.IsFiniteRelIndex (Matrix.SpecialLinearGroup.mapGL โ„).range] {k : โ„ค} (f : ModularForm ๐’ข k) [DiscreteTopology โ†ฅ๐’ข.strictPeriods] (h : โ†‘((k * โ†‘(Nat.card (โ†ฅ(Matrix.SpecialLinearGroup.mapGL โ„).range โงธ ๐’ข.subgroupOf (Matrix.SpecialLinearGroup.mapGL โ„).range))).toNat / 12) < (UpperHalfPlane.qExpansion ๐’ข.strictWidthInfty โ‡‘f).order) :
f = 0

Sturm bound for subgroups of GL(2, โ„) of finite relative index in SL(2, โ„ค) with discrete strict periods. A modular form of weight k whose q-expansion at the cusp โˆž has order strictly greater than k ยท [๐’ฎโ„’ : ๐’ข โŠ“ ๐’ฎโ„’] / 12 is identically zero.

source
theorem TauCeti.ModularForm.sturm_bound_finiteIndex_SL2Z {ฮ“ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) โ„ค)} [ฮ“.FiniteIndex] {k : โ„ค} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL โ„) ฮ“) k) (h : โ†‘((k * โ†‘ฮ“.index).toNat / 12) < (UpperHalfPlane.qExpansion (Subgroup.map (Matrix.SpecialLinearGroup.mapGL โ„) ฮ“).strictWidthInfty โ‡‘f).order) :
f = 0

Classical Sturm bound for finite-index subgroups of SL(2, โ„ค).

source
theorem TauCeti.ModularForm.eq_of_sturm_bound {๐’ข : Subgroup (GL (Fin 2) โ„)} [๐’ข.IsFiniteRelIndex (Matrix.SpecialLinearGroup.mapGL โ„).range] {k : โ„ค} (f : ModularForm ๐’ข k) [DiscreteTopology โ†ฅ๐’ข.strictPeriods] (g : ModularForm ๐’ข k) (h : โˆ€ i โ‰ค (k * โ†‘(Nat.card (โ†ฅ(Matrix.SpecialLinearGroup.mapGL โ„).range โงธ ๐’ข.subgroupOf (Matrix.SpecialLinearGroup.mapGL โ„).range))).toNat / 12, (PowerSeries.coeff i) (UpperHalfPlane.qExpansion ๐’ข.strictWidthInfty โ‡‘f) = (PowerSeries.coeff i) (UpperHalfPlane.qExpansion ๐’ข.strictWidthInfty โ‡‘g)) :
f = g

Modular forms agreeing up to the Sturm bound are equal: two weight-k forms whose q-expansions at โˆž agree in every coefficient up to k ยท [๐’ฎโ„’ : ๐’ข โŠ“ ๐’ฎโ„’] / 12 coincide.

source
instance TauCeti.ModularForm.finiteDimensional_modularForm_finiteIndex {๐’ข : Subgroup (GL (Fin 2) โ„)} [๐’ข.HasDetOne] [๐’ข.IsFiniteRelIndex (Matrix.SpecialLinearGroup.mapGL โ„).range] [DiscreteTopology โ†ฅ๐’ข.strictPeriods] {k : โ„ค} :
Module.Finite โ„‚ (ModularForm ๐’ข k)

Finite-dimensionality of modular forms. As a corollary of the Sturm bound, the space ModularForm ๐’ข k is finite-dimensional over โ„‚ for any subgroup ๐’ข โ‰ค GL(2, โ„) of finite relative index in ๐’ฎโ„’ with determinant-one elements and discrete strict periods.

source
instance TauCeti.finiteDimensional_cuspForm_finiteIndex {๐’ข : Subgroup (GL (Fin 2) โ„)} [๐’ข.HasDetOne] [๐’ข.IsFiniteRelIndex (Matrix.SpecialLinearGroup.mapGL โ„).range] [DiscreteTopology โ†ฅ๐’ข.strictPeriods] {k : โ„ค} :
Module.Finite โ„‚ (CuspForm ๐’ข k)

Finite-dimensionality of cusp forms. A cusp form is a modular form, injectively, so this is TauCeti.ModularForm.finiteDimensional_modularForm_finiteIndex transported along CuspForm.toModularFormโ‚—, under exactly the same hypotheses.

It is stated here rather than at its use sites because cusp-form finite-dimensionality is a standing hypothesis of the old/new theory, not a fact local to any one argument: before this, the two proofs in TauCeti/NumberTheory/ModularForms/Petersson/Orthogonal.lean that need it each built it inline.