Core Identity for the Valence Formula #
The orbit-sum valence formula applied to the canonical zero set s₀.
Main Results #
valence_formula_orbit_sum— orbit-sum with boundary weight hypothesis
theorem
valence_formula_orbit_sum
{k : ℤ}
(f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k)
(hf : f ≠ 0)
(S : Finset UpperHalfPlane)
(hS : ∀ p ∈ S, p ∈ ModularGroup.fd)
(hS_complete : ∀ p ∈ ModularGroup.fd, orderOfVanishingAt' (⇑f) p ≠ 0 → p ∈ S)
:
↑(orderAtCusp' f) + 1 / 2 * ↑(orderOfVanishingAt' (⇑f) ellipticPointI') + 1 / 3 * ↑(orderOfVanishingAt' (⇑f) ellipticPointRho') + ∑ s ∈ S with
s ≠ ellipticPointI' ∧ s ≠ ellipticPointRho' ∧ s ≠ ellipticPointRhoPlusOne' ∧ ‖↑s‖ > 1 ∧ |(↑s).re| < 1 / 2,
↑(orderOfVanishingAt' (⇑f) s) + ∑ s ∈ sLeftVert S, ↑(orderOfVanishingAt' (⇑f) s) + ∑ s ∈ S with s ≠ ellipticPointRho' ∧ ‖↑s‖ = 1 ∧ (↑s).re < 0, ↑(orderOfVanishingAt' (⇑f) s) = ↑k / 12
Orbit-sum valence formula with boundary weight hypothesis.