$\DeclareMathOperator\ord{ord}\DeclareMathOperator\Im{Im}$La fórmula de valencia para una forma modular establece que si $f: \mathbf{H} \to \mathbf{C}$ es una forma modular de peso $k$ en el semiplano superior ${\mathbf H} := \{ z: \Im z > 0 \}$ en el sentido de que $$ f\left(\frac{az+b}{cz+d}\right) = (cz+d)^k f(z)$$ para todo $\begin{pmatrix} a & b \\ c & d \end{pmatrix} \in SL_2({\bf Z})$, y $f$ es holomorfa en todo ${\mathbf H}$ y también acotada cuando $\Im z \to \infty$ entonces (si $f$ no es identicamente cero) se tiene la identidad $$ \sum_\rho \ord_\rho(f) + \ord_\infty(f) + \frac{1}{2} \ord_i(f) + \frac{1}{3} \ord_{e^{\pi i/3}}(f) = \frac{k}{12}$$ donde $\rho$ varía sobre los ceros de $f$ lejos de los puntos fijos (parcialmente) $i, e^{\pi i/3}, \infty$ de la acción, con cada órbita de $\operatorname{SL}_2(\mathbf{Z})$ evitando estos puntos fijos que se representa precisamente una vez en esta suma, y el orden de desaparición en el infinito definido en términos de la variable del nomo (al cuadrado) $q = e^{2\pi i z}$.
La demostración estándar de esta identidad procede integrando el logaritmo del derivado de $f'/f$ en un contorno algo complicado diseñado para evitar ceros, y que se ve algo así (imagen tomada de esta fuente):
La afirmación entonces sigue de una aplicación rutinaria del teorema de los residuos, después de estimar adecuadamente la contribución de los diversos componentes del contorno.
Resulta que este argumento, aunque directo, es algo difícil de formalizar en lenguajes de asistentes de prueba; vea la discusión en las diapositivas anteriormente vinculadas. ¿Existen otras pruebas de esta fórmula que no se basen en una integración de contorno complicada? He experimentado con un enfoque tipo fórmula de Green en la que $f'/f$ se integra contra una función de corte adecuada, digamos en el disco unitario en la variable del nomo (al cuadrado) $q = e^{2\pi i z}$, pero los cálculos son bastante complicados. También se puede obtener esta fórmula usando la coordenada del $j$-invariante para modular la curva, aunque esto es algo circular ya que a menudo se necesita la fórmula de valencia para establecer propiedades de este invariante. También consideré intentar usar herramientas generales de superficies de Riemann como la fórmula de Riemann-Hurwitz, pero entre otras cosas me encontré con la necesidad de triangularizar una superficie de Riemann, lo cual también sería complicado de formalizar creo.
