Definitions/Def_CuspForm_Petersson.lean

Fix a level N and a weight k \in \mathbb{Z}, and let f, g be cusp forms of weight k for \Gamma_0(N) (Mathlib's CuspForm (CongruenceSubgroup.Gamma0 N) k). Two definitions are made. First, CuspForm.peterssonIntegrand f g is the function on the upper half-plane whose value at \tau is the sum, over the coset space \mathrm{SL}(2,\mathbb{Z}) \mathbin{/} \Gamma_0(N), of the pointwise Petersson densities \overline{(f\mid_k \sigma^{-1})(\tau)}\,(g\mid_k \sigma^{-1})(\tau)\,(\operatorname{Im}\tau)^k, where \sigma runs through the chosen representatives q.out of the cosets q, the weight-k slash action is Mathlib's ∣[k] and the density is Mathlib's UpperHalfPlane.petersson. The sum is the finitely-supported sum ∑ᶠ, so for N \ge 1, where the coset space is finite, it is the ordinary finite sum of [\mathrm{SL}(2,\mathbb{Z}) : \Gamma_0(N)] terms; for families without finite support the ∑ᶠ convention returns 0, which is all that is asserted when the index is infinite. Second, CuspForm.petersson f g is the integral of this integrand over ModularGroup.fd, the standard fundamental domain for \mathrm{SL}(2,\mathbb{Z}) acting on \mathbb{H}, taken with respect to the volume measure of the upper half-plane restricted to that set, i.e. the hyperbolic measure y^{-2}\,dx\,dy. Unfolding, this is the Petersson product \langle f, g\rangle = \int_{\Gamma_0(N)\backslash\mathbb{H}} \overline{f(\tau)}\,g(\tau)\,(\operatorname{Im}\tau)^k\,\frac{dx\,dy}{y^2}, realised by unfolding the quotient by \Gamma_0(N) into an \mathrm{SL}(2,\mathbb{Z})-invariant integrand on a fundamental domain for the full modular group; in particular no normalising factor 1/[\mathrm{SL}(2,\mathbb{Z}) : \Gamma_0(N)] and no factor of the volume of the quotient is inserted. The definition is conjugate-linear in f and linear in g. The auxiliary CuspForm.petersson_def restates the defining equation as an equality of terms.