Integrals of one-forms along geodesics between cusps

For F : ℍ → ℂ and a rational matrix g ∈ GL(2, ℚ) of positive determinant, the geodesic from the cusp g • 0 to the cusp g • ∞ is the image under g of the positive imaginary axis, and the substitution z = g • (i t) turns the integral of the one-form F(z) dz along it into

∫_{g • 0}^{g • ∞} F(z) dz = i ∫₀^∞ (F ∣[2] g)(i t) dt,

because the weight-2 slash (F ∣[2] g)(τ) = F(g • τ) · det g · (cτ + d)⁻² is exactly the pullback of F(z) dz along τ ↦ g • τ. This file takes the right-hand side as the definition of the geodesic integral Matrix.GeneralLinearGroup.geodesicIntegral g F and proves that it is intrinsic to the oriented geodesic: it depends only on the pair of endpoints (g • 0, g • ∞), changes sign when the endpoints are swapped, and transforms under a further matrix by slashing the integrand. Both endpoints are improper, and the integral is a Bochner integral, so it vanishes when the integrand is not integrable; the convergence criterion UpperHalfPlane.integrableOn_resToImagAxis_Ioi_of_slash_S (in TauCeti.NumberTheory.ModularForms.ResToImagAxis) reduces integrability near the finite end g • 0 to integrability near i∞ of the reflected integrand F ∣[2] (g S), so that both ends are handled by decay at i∞.

The definition is total in g, following the convention of the rational slash action itself (TauCeti.NumberTheory.ModularForms.SlashActionRat) and of the Hecke modules, which work in GL(2, ℚ) and assume 0 < det g where they need it. For det g < 0 the value is the same formula, but Mathlib's slash then involves complex conjugation, so it is not the integral of F(z) dz along the geodesic from g • 0 to g • ∞: every statement below whose content is geometric — dependence on the endpoints only, ℂ-linearity, convergence — carries the hypothesis 0 < det g, and the identities stated for all g (geodesicIntegral_mul, geodesicIntegral_mul_S, additivity) are algebraic consequences of the slash action, whose geometric reading likewise requires positive determinant.

These integrals are the raw material of the period pairing between cusp forms and modular symbols, whose integrand f(z) P(z, 1) and convergence are treated in TauCeti.NumberTheory.ModularForms.ModularSymbols.Period.Integral.

Main definitions

• Matrix.GeneralLinearGroup.geodesicIntegral g F: the integral ∫_{g • 0}^{g • ∞} F(z) dz, as i ∫₀^∞ (F ∣[2] g)(i t) dt. It is an operation on the matrix g ∈ GL(2, ℚ) cutting out the geodesic, so it lives in the namespace of GL and is available as g.geodesicIntegral F.

Main results

• Matrix.GeneralLinearGroup.geodesicIntegral_mul: the substitution z ↦ g • z, ∫_{gh • 0}^{gh • ∞} F(z) dz = ∫_{h • 0}^{h • ∞} (F ∣[2] g)(z) dz.
• Matrix.GeneralLinearGroup.geodesicIntegral_mul_of_diagonal and Matrix.GeneralLinearGroup.geodesicIntegral_eq_of_smul_eq: the integral only depends on the endpoints g • 0 and g • ∞, for g of positive determinant.
• Matrix.GeneralLinearGroup.geodesicIntegral_mul_S: reversing the orientation, ∫_{g • ∞}^{g • 0} F(z) dz = -∫_{g • 0}^{g • ∞} F(z) dz.
• Matrix.GeneralLinearGroup.geodesicIntegral_add and Matrix.GeneralLinearGroup.geodesicIntegral_smul: linearity in the integrand, for integrable integrands.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, §8.2.
• Y. I. Manin, Parabolic points and zeta functions of modular curves, Izv. Akad. Nauk SSSR Ser. Mat. 36 (1972), 19–66, §1.

noncomputable def Matrix.GeneralLinearGroup.geodesicIntegral (g : GL (Fin 2) ℚ) (F : UpperHalfPlane → ℂ) : ℂ

The integral ∫_{g • 0}^{g • ∞} F(z) dz of the one-form F(z) dz along the hyperbolic geodesic from the cusp g • 0 to the cusp g • ∞, for g ∈ GL(2, ℚ) of positive determinant: that geodesic is the g-image of the positive imaginary axis, and substituting z = g • (i t) gives i ∫₀^∞ (F ∣[2] g)(i t) dt, the imaginary-axis integral of the weight-2 slash of F. Both endpoints are improper, and the Bochner integral is 0 when the integrand is not integrable.

The definition is total in g, like the slash action: for det g < 0 it is the same formula, which is then a junk value and not the integral along the geodesic from g • 0 to g • ∞ (the slash of a negative-determinant matrix involves complex conjugation). Every result reading it as a geodesic integral assumes 0 < det g.

Equations

• g.geodesicIntegral F = Complex.I * ∫ (t : ℝ) in Set.Ioi 0, UpperHalfPlane.resToImagAxis (SlashAction.map 2 g F) t

theorem Matrix.GeneralLinearGroup.geodesicIntegral_def (g : GL (Fin 2) ℚ) (F : UpperHalfPlane → ℂ) : g.geodesicIntegral F = Complex.I * ∫ (t : ℝ) in Set.Ioi 0, UpperHalfPlane.resToImagAxis (SlashAction.map 2 g F) t

Definition of the geodesic integral.

theorem Matrix.GeneralLinearGroup.geodesicIntegral_mul (g h : GL (Fin 2) ℚ) (F : UpperHalfPlane → ℂ) : (g * h).geodesicIntegral F = h.geodesicIntegral (SlashAction.map 2 g F)

The substitution z ↦ g • z: the integral of F(z) dz from gh • 0 to gh • ∞ is the integral of the pulled-back one-form (F ∣[2] g)(z) dz from h • 0 to h • ∞. The identity is an algebraic consequence of the slash action and holds for every g and h; its reading as a substitution in a geodesic integral requires g and h to have positive determinant.

@[simp]

theorem Matrix.GeneralLinearGroup.geodesicIntegral_zero (g : GL (Fin 2) ℚ) : g.geodesicIntegral 0 = 0

The geodesic integral of the zero one-form vanishes.

theorem Matrix.GeneralLinearGroup.geodesicIntegral_add (g : GL (Fin 2) ℚ) {F G : UpperHalfPlane → ℂ} (hF : MeasureTheory.IntegrableOn (UpperHalfPlane.resToImagAxis (SlashAction.map 2 g F)) (Set.Ioi 0) MeasureTheory.volume) (hG : MeasureTheory.IntegrableOn (UpperHalfPlane.resToImagAxis (SlashAction.map 2 g G)) (Set.Ioi 0) MeasureTheory.volume) : g.geodesicIntegral (F + G) = g.geodesicIntegral F + g.geodesicIntegral G

The geodesic integral is additive in the integrand, for integrable integrands (for every g, since the slash action is additive).

theorem Matrix.GeneralLinearGroup.geodesicIntegral_smul {g : GL (Fin 2) ℚ} (hg : 0 < (↑g).det) (c : ℂ) (F : UpperHalfPlane → ℂ) : g.geodesicIntegral (c • F) = c * g.geodesicIntegral F

The geodesic integral is ℂ-linear in the integrand, for g of positive determinant (for negative determinant the slash conjugates the scalar).

Independence of the parametrisation

theorem Matrix.GeneralLinearGroup.geodesicIntegral_mul_of_diagonal (g : GL (Fin 2) ℚ) {d : GL (Fin 2) ℚ} (h₁₀ : ↑d 1 0 = 0) (h₀₁ : ↑d 0 1 = 0) (hd : 0 < (↑d).det) (F : UpperHalfPlane → ℂ) : (g * d).geodesicIntegral F = g.geodesicIntegral F

Reparametrising the geodesic. A diagonal matrix d of positive determinant fixes the cusps 0 and ∞ and rescales the imaginary axis, so it does not change the geodesic integral from g • 0 to g • ∞.

theorem Matrix.GeneralLinearGroup.geodesicIntegral_eq_of_smul_eq {g g' : GL (Fin 2) ℚ} (hg : 0 < (↑g).det) (hg' : 0 < (↑g').det) (h₀ : g • ↑0 = g' • ↑0) (hinf : g • OnePoint.infty = g' • OnePoint.infty) (F : UpperHalfPlane → ℂ) : g.geodesicIntegral F = g'.geodesicIntegral F

The geodesic integral only depends on the endpoints. Two matrices of positive determinant sending (0, ∞) to the same pair of cusps give the same integral.

Reversing the orientation

theorem Matrix.GeneralLinearGroup.geodesicIntegral_mul_S (g : GL (Fin 2) ℚ) (F : UpperHalfPlane → ℂ) : (g * (SpecialLinearGroup.mapGL ℚ) ModularGroup.S).geodesicIntegral F = -g.geodesicIntegral F

Reversing the orientation of the geodesic: g S sends (0, ∞) to (g • ∞, g • 0), and the integral from g • ∞ to g • 0 is the negative of the integral from g • 0 to g • ∞. The identity is the substitution t ↦ 1 / t on the imaginary axis and holds for every g; its reading as an orientation reversal of a geodesic integral requires 0 < det g.