Textbook Orbit-Finsum Form of the Valence Formula

This file proves the valence formula in literal orbit-sum form using ∑ᶠ over non-elliptic orbits of SL₂(ℤ) acting on ℍ.

Main Results

• valence_formula_textbook_orbit_finsum — the valence formula with ∑ᶠ

noncomputable def ordOrbitQ {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (q : NonEllOrbit) : ℂ

The order of vanishing on non-elliptic orbits, cast to ℂ.

Equations

• ordOrbitQ f q = ↑(ordOrbit f ↑q)

theorem finsum_nonell_eq_repCanon_sum {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) : ∑ᶠ (q : NonEllOrbit), ordOrbitQ f q = ∑ s ∈ repCanon f hf, ↑(orderOfVanishingAt' (⇑f) s)

The finsum over non-elliptic orbits equals the repCanon sum.

theorem valence_formula_textbook_orbit_finsum {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) : ↑(orderAtCusp' f) + 1 / 2 * ↑(orderOfVanishingAt' (⇑f) ellipticPointI') + 1 / 3 * ↑(orderOfVanishingAt' (⇑f) ellipticPointRho') + ∑ᶠ (q : NonEllOrbit), ordOrbitQ f q = ↑k / 12

The valence formula as an orbit-sum with ∑ᶠ over non-elliptic orbits.