The cusp term of the general-level valence formula #

For 𝒢 ≤ GL(2, ℝ) of finite relative index in 𝒮ℒ, the norm ModularForm.norm 𝒮ℒ f = ∏_{q ∈ 𝒮ℒ ⧸ 𝒢 ⊓ 𝒮ℒ} f ∣[k] q⁻¹ of a weight-k form on 𝒢 is a level-one form, and TauCeti/NumberTheory/ModularForms/Norm/Valence.lean reads the level-one valence formula back along it as

Σ_{P ∈ 𝒢 \ ℍ} (2 / |Stab_𝒢 P|) · ord_P f + ord_∞(Nm f) = k · [SL(2, ℤ) : 𝒢] / 12,

whose cusp term is still one order at ∞, taken on the norm. This file distributes that term over the cusps of 𝒢, each read in its own width parameter, and so closes the general-level valence formula (valence_formula_finiteIndex).

Indexing the cusp translation orbits #

The coset of x contributes the factor f ∣[k] x⁻¹, which is f read at the cusp x⁻¹ ∞, and two cosets contribute at the same cusp exactly when they differ by left multiplication by an element of the stabiliser ⟨T, -I⟩ of ∞ in SL(2, ℤ). Here the cusp term is indexed by the orbits of ⟨T⟩ alone (CuspTranslationOrbit), so a classical cusp of 𝒢 corresponds to one cusp translation orbit or two, according as its ⟨T⟩-orbit is stable under -I or not. That is the full-coset convention that Norm/Valence.lean already makes on the interior term — the weight there is read on the matrix stabiliser, and the norm's weight is k · [SL(2, ℤ) : 𝒢] for the full index — so both halves of the identity are read for the full coset space, which is what makes them match.

The width of an orbit is the period of that action: the least m > 0 with x⁻¹ T ^ m x ∈ 𝒢 (minimalPeriod_TSL_dvd_iff, cuspTranslationOrbitWidth_mk). It is the classical width of the cusp x⁻¹ ∞ when -I ∈ 𝒢, and otherwise that width or twice it, in step with the same convention. The widths sum to the index (sum_cuspTranslationOrbitWidth), and the orbit of the base coset — the cusp ∞ — has width Subgroup.integerCuspWidth 𝒢 (cuspTranslationOrbitWidth_mk_one).

The mechanism #

Over one orbit the coset factors are the integer translates of a single factor, so they multiply to the Galois product galoisProd of it; and the width-1 expansion of a Galois product has the same order as the width-m expansion of the function it is built from (qExpansion_one_galoisProd_order_eq). The norm is the product of these Galois products over the orbits, so its order at ∞ is the sum of the orders of f at the cusp translation orbits. Nothing here divides by an order that could be ⊤: each factor of a nonzero form is nonzero (SlashInvariantForm.quotientFunc_ne_zero), which is what the additivity of qExpansionOrderAtCusp over products asks for.

Main definitions #

TauCeti.ModularForm.CuspTranslationOrbit: the T-orbits on 𝒮ℒ ⧸ 𝒢 ⊓ 𝒮ℒ that index the cusp term under the full-coset convention.
TauCeti.ModularForm.cuspTranslationOrbitWidth: the width of a cusp translation orbit.
TauCeti.ModularForm.orderAtCuspTranslationOrbit: the vanishing order of a form at a cusp translation orbit, read in that orbit's width.

Main results #

TauCeti.ModularForm.orderAtCuspTranslationOrbit_mk: the order at an orbit may be read at any representative coset, so the Quotient.out of the definition is only a spelling.
TauCeti.ModularForm.qExpansionOrderAtCusp_one_norm_eq_sum_orderAtCuspTranslationOrbit: the cusp distribution — ord_∞(Nm f) = Σ_c ord_c f.
TauCeti.ModularForm.valence_formula_finiteIndex: the valence formula at general level, with both halves distributed.
TauCeti.ModularForm.twelve_mul_orderAtCuspTranslationOrbit_le_weight_mul_index: the mass at one cusp translation orbit is bounded by the total mass.

References #

F. Diamond and J. Shurman, A first course in modular forms, §3.