The vanishing order on SL(2, ℤ)-orbits #
The vanishing order of a level-one modular form is constant on SL(2, ℤ)-orbits of ℍ,
so it descends to the orbit space (TauCeti.ModularForm.orderOfVanishingOnOrbit), and only
finitely many orbits carry nonzero order — the summation index of the valence formula. No
nonvanishing hypothesis is needed: the zero form has order 0 on every orbit, so its support is
empty. The generic orbit facts it rides live in TauCeti.NumberTheory.Modular.Orbits.
Main declarations #
TauCeti.ModularForm.orderOfVanishingOnOrbit: the order descended toMulAction.orbitRel.Quotient SL(2, ℤ) ℍ.TauCeti.ModularForm.orderOfVanishingOnOrbit_nonneg: the order on an orbit is nonnegative.TauCeti.ModularForm.hasFiniteSupport_orderOfVanishingOnOrbit: finite support on orbits, the zero form having empty support.TauCeti.ModularForm.weightedOrderOfVanishingOnOrbit: the elliptic-weighted orderord_P f / e_P, together with its values and finite-support properties.TauCeti.ModularForm.finsum_weightedOrderOfVanishingOnOrbit_eq_finsum_nonElliptic_add_elliptic: the uniform weighted sum split into its non-elliptic and two elliptic parts.TauCeti.ModularForm.sum_orderOfVanishingAt_eq_finsum_orbit: a divisor sum over an arbitrary index set, reindexed over the orbits its points represent, given that the index-to-orbit composite is injective.TauCeti.ModularForm.sum_orderOfVanishingAt_ofComplex_eq_finsum_orbit: the same for the valence formula's own divisor sum, whose points are complex numbers carrying the interior bounds.TauCeti.ModularForm.orderOfVanishingOnOrbit_eq_zero_of_notMem: an orbit outside a set of orbits complete forf's nonzero-order points on𝒟carries vanishing order zero.TauCeti.ModularForm.NonEllipticOrbit: the orbits other than those of the elliptic pointsiandρ— the index type of the valence formula's divisor sum.TauCeti.ModularForm.hasFiniteSupport_orderOfVanishingOnOrbit_nonElliptic: the finite support restricted to the non-elliptic orbits.
References #
- AINTLIB
LeanModularForms— the valence-formula development this file ports onto the current Mathlib pin. - F. Diamond and J. Shurman, A first course in modular forms, Chapter 3 — the elliptic-weighted divisor summand; new here, not part of the AINTLIB port above.
The vanishing order of a level-one form, descended to SL(2, ℤ)-orbits of ℍ.
Equations
Instances For
Evaluating the descended order on the orbit of p recovers the vanishing order at
p.
The vanishing order on an orbit is nonnegative: a modular form is holomorphic, so it has no poles.
Only finitely many orbits of a level-one form carry nonzero order.
The elliptic-weighted order #
The elliptic-weighted vanishing order of f on an orbit: ord_P f / e_P, the summand
of the valence formula in its uniform form ∑_P (1 / e_P) · ord_P f + ord_∞ f = k / 12. The
weight is 1 on all but the two elliptic orbits, where it is 1/2 and 1/3.
Equations
Instances For
The defining equation for the elliptic-weighted vanishing order.
Evaluating the weighted order on the orbit of p recovers the pointwise order divided by
the elliptic order of that orbit.
Off the two elliptic orbits the weight is 1, so the summand is the plain order.
At the orbit of i the weight is 1/2, from e_i = 2.
At the orbit of ρ the weight is 1/3, from e_ρ = 3.
Multiplying the weighted order by the elliptic order recovers the plain vanishing order.
Every elliptic-weighted order is nonnegative: a modular form is holomorphic and the weights are positive.
Only finitely many orbits have nonzero elliptic-weighted order: the weight cannot create support where the order has none.
A divisor sum reindexed over the orbits its points represent. The index set is arbitrary,
mapped into ℍ by p.
The hypothesis is that the composite a ↦ ⟦p a⟧ is injective on X, which is what makes the
reindexing lossless. That is strictly more than asking the orbit map to be injective on p '' X:
it also rules out distinct indices with the same p, since those would contribute twice on the
left and once on the right.
For p injective — ofComplex on the upper half plane, say — the composite's injectivity
reduces to the orbit map's, which ModularGroup.orbit_mk_injOn_fdo.mono supplies on the open
fundamental domain. The open domain is genuinely needed there: on the closed 𝒟 the orbit map is
not injective, since T identifies the two vertical edges and S the two halves of the arc, so a
set holding two identified boundary representatives would count their common orbit twice.
The divisor sum of the valence formula, whose points are complex numbers carrying the
interior bounds, reindexed over the orbits they represent — the case p := ofComplex of
sum_orderOfVanishingAt_eq_finsum_orbit.
The index is a Set image rather than a Finset one, which keeps the statement free of a
classical DecidableEq (MulAction.orbitRel.Quotient SL(2, ℤ) ℍ) instance — the image elements are
orbits, so that, not DecidableEq ℍ, is what a Finset image would need.
The three hypotheses are the interior bounds the valence formula carries: positivity puts each
point in ℍ, and the radial and real-part bounds put it in the open fundamental domain, where
distinct points represent distinct orbits.
The missing completeness step. An orbit outside a set S that catches every
fundamental-domain point of nonzero order carries vanishing order zero. Completeness means hS:
every p ∈ 𝒟 with orderOfVanishingAt f p ≠ 0 has its orbit ⟦p⟧ inside S, the same idiom
hasFiniteSupport_orderOfVanishingOnOrbit uses over 𝒟.
⚠ This does not by itself extend sum_orderOfVanishingAt_ofComplex_eq_finsum_orbit's
image-indexed ∑ᶠ to the whole orbit space. Instantiated at that lemma's orbit map, hS ranges
over the closed 𝒟, which holds the elliptic points i and ρ (‖i‖ = ‖ρ‖ = 1), whereas that
lemma confines its divisor set to the open 𝒟ᵒ. For a form of nonzero order at i or ρ the
two demands cannot both hold — those are exactly the points the valence formula weights by 1/2
and 1/3 instead of counting into the divisor sum. Reaching the roadmap's non-elliptic orbit
space still needs separate treatment of the elliptic orbits.
The non-elliptic orbits of SL(2, ℤ) on ℍ: all orbits except the two elliptic ones, of
i and of ρ. The valence formula's divisor sum is indexed by this type — the elliptic
orbits enter the formula through fractional weights instead.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Only finitely many non-elliptic orbits of a level-one form carry nonzero order: the finite
support of orderOfVanishingOnOrbit, restricted along the inclusion of the non-elliptic
orbits.
Splitting the uniform divisor sum at the two elliptic orbits. Away from them the weight
is 1, so the sum over all orbits is the non-elliptic sum plus the two weighted elliptic terms.