The slash action on the imaginary axis

The restriction UpperHalfPlane.resToImagAxis of a function on ℍ to the positive imaginary axis intertwines the weight-k slash action of S = ![![0, -1], ![1, 0]] with the involution t ↦ 1 / t of the axis. This is the reflection underlying the functional equation of the L-function of a modular form, and, in weight 2, the change of variables that moves the finite endpoint of a geodesic between cusps to i∞.

A cusp form slashed by a rational matrix is a cusp form on the conjugate arithmetic level, so its restriction to the imaginary axis decays exponentially; this is the convergence input for integrals of cusp forms along geodesics between cusps.

Main results

• UpperHalfPlane.resToImagAxis_slash_S: the restriction of F ∣[k] S at t is i ^ (-k) t ^ (-k) times the restriction of F at 1 / t, and UpperHalfPlane.resToImagAxis_slash_two_S: in weight 2 this is -t⁻² times the restriction of F at 1 / t.
• UpperHalfPlane.integrableOn_resToImagAxis_Ioi_of_slash_S: a function whose restriction is integrable near i∞ and whose weight-2 S-reflection is also integrable near i∞ has restriction integrable along the whole positive imaginary axis.
• UpperHalfPlane.resToImagAxis_slash_two_of_diagonal: in weight 2, the restriction of F ∣[2] d for a positive diagonal rational matrix d = diag(a, b) at t is r times the restriction of F at r t, where r = a / b.
• UpperHalfPlane.exists_isBigO_rat_slash_exp: for a cusp form f on an arithmetic subgroup and g ∈ GL(2, ℚ), f ∣[k] g is O(exp (-c Im τ)) at i∞ for some c > 0, and UpperHalfPlane.exists_isBigO_resToImagAxis_rat_slash_exp: its restriction to the imaginary axis is O(exp (-c t)).

Ported from the AINTLIB LeanModularForms project (LeanModularForms/Modularforms/ResToImagAxis.lean, Chris Birkbeck, https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms); the generic material about the restriction is in TauCeti/Analysis/Complex/UpperHalfPlane/ResToImagAxis.lean.

theorem UpperHalfPlane.resToImagAxis_slash_S (F : UpperHalfPlane → ℂ) (k : ℤ) {t : ℝ} (ht : 0 < t) : resToImagAxis (SlashAction.map k ModularGroup.S F) t = Complex.I ^ (-k) * ↑t ^ (-k) * resToImagAxis F (1 / t)

The S-involution on the imaginary axis: slashing by S turns t into 1 / t, (F ∣[k] S) (i t) = i ^ (-k) t ^ (-k) F (i / t). This is the reflection underlying the functional equation of the L-function.

theorem UpperHalfPlane.resToImagAxis_slash_two_S (F : UpperHalfPlane → ℂ) {t : ℝ} (ht : 0 < t) : resToImagAxis (SlashAction.map 2 ModularGroup.S F) t = -(↑t ^ 2)⁻¹ * resToImagAxis F t⁻¹

The S-involution in weight 2: (F ∣[2] S) (i t) = -t⁻² F (i / t), the reflection t ↦ 1 / t of the axis together with its Jacobian.

theorem UpperHalfPlane.integrableOn_resToImagAxis_Ioi_of_slash_S {G : UpperHalfPlane → ℂ} (h : MeasureTheory.IntegrableOn (resToImagAxis G) (Set.Ici 1) MeasureTheory.volume) (hS : MeasureTheory.IntegrableOn (resToImagAxis (SlashAction.map 2 ModularGroup.S G)) (Set.Ici 1) MeasureTheory.volume) : MeasureTheory.IntegrableOn (resToImagAxis G) (Set.Ioi 0) MeasureTheory.volume

Convergence at the finite end from convergence at i∞ of the reflection. If the restriction of G to the imaginary axis is integrable near i∞, and so is that of the weight-2 reflection G ∣[2] S, then the restriction of G is integrable on the whole positive axis: the substitution t ↦ 1 / t carries the tail of G ∣[2] S onto the initial segment of G.

theorem UpperHalfPlane.resToImagAxis_slash_two_of_diagonal (F : UpperHalfPlane → ℂ) {d : GL (Fin 2) ℚ} (h₁₀ : ↑d 1 0 = 0) (h₀₁ : ↑d 0 1 = 0) (hd : 0 < (↑d).det) (t : ℝ) : resToImagAxis (SlashAction.map 2 d F) t = ↑(↑(↑d 0 0) / ↑(↑d 1 1)) * resToImagAxis F (↑(↑d 0 0) / ↑(↑d 1 1) * t)

A positive diagonal matrix rescales the imaginary axis: for d = diag(a, b) ∈ GL(2, ℚ) with ab > 0, the weight-2 slash by d restricts to the axis as (F ∣[2] d) (i t) = r F (i r t) with r = a / b > 0, the rescaling t ↦ r t of the axis together with its Jacobian.

theorem UpperHalfPlane.exists_isBigO_rat_slash_exp {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} [CuspFormClass F Γ k] (f : F) (g : GL (Fin 2) ℚ) : ∃ c > 0, SlashAction.map k g ⇑f =O[atImInfty] fun (τ : UpperHalfPlane) => Real.exp (-c * τ.im)

A cusp form slashed by a rational matrix decays exponentially at i∞: f ∣[k] g is a cusp form on the conjugate level g⁻¹ Γ g, which is again arithmetic, so it has the exponential decay of a cusp form at i∞, uniformly in the real part.

theorem UpperHalfPlane.exists_isBigO_resToImagAxis_rat_slash_exp {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} [CuspFormClass F Γ k] (f : F) (g : GL (Fin 2) ℚ) : ∃ c > 0, resToImagAxis (SlashAction.map k g ⇑f) =O[Filter.atTop] fun (t : ℝ) => Real.exp (-c * t)

A cusp form slashed by a rational matrix decays exponentially along the imaginary axis, the restriction of exists_isBigO_rat_slash_exp to the axis.