The transformation law of the Eichler integral

Let f be a cusp form of weight k = n + 2 and E_f = E_{n+1} f its Eichler integral (TauCeti.eichlerIntegral), which by TauCeti.CuspFormClass.eichlerIntegral_eq_integral is

E_f(τ) = (-2πi)ⁿ⁺¹ / n! · ∫_τ^{i∞} f(z) (z - τ)ⁿ dz.

This file proves that E_f transforms in weight 2 - k = -n up to a period polynomial: for σ ∈ SL(2, ℤ),

(E_f ∣[-n] σ)(τ) = E_{f ∣[k] σ}(τ) - (-2πi)ⁿ⁺¹ / n! · ∫_{σ⁻¹ • ∞}^{i∞} (f ∣[k] σ)(z) (z - τ)ⁿ dz,

where the last integral is a period of f ∣[k] σ along the geodesic between two cusps, and so, by TauCeti.ModularSymbols.cuspIntegral_mul_sub_pow, a polynomial in τ of degree at most n whose coefficients are the periods ∫ (f ∣[k] σ)(z) zʲ dz. The proof substitutes z ↦ σ • z in the integral from σ • τ to i∞: since σ • z - σ • τ = (z - τ) / ((cz + d)(cτ + d)), this turns f(z) (z - σ • τ)ⁿ dz into (cτ + d)⁻ⁿ (f ∣[k] σ)(z) (z - τ)ⁿ dz, and moves the path to one from τ to the cusp σ⁻¹ • ∞, which is compared with the vertical ray from τ by TauCeti.integral_Ioi_slash_eq_add_cuspIntegral.

For σ in the level of f the form f ∣[k] σ is f itself, and the law reads E_f ∣[-n] σ - E_f = (period polynomial of f at σ). In particular, if the periods of f vanish then E_f is invariant in weight -n under the level. This is the first step of the proof that a cusp form of weight k ≥ 2 with vanishing periods is zero (the injectivity of the Eichler–Shimura period map): such an E_f is then a holomorphic form of nonpositive weight. For σ outside the level, f ∣[k] σ is a cusp form for a conjugate subgroup, and the general law compares E_f ∣[-n] σ with its Eichler integral, which is what controls E_f at the cusp σ • ∞.

Main results

• TauCeti.CuspFormClass.eichlerIntegral_slash_apply: the transformation law under σ ∈ SL(2, ℤ), for a cusp form f' with f' = f ∣[k] σ.
• TauCeti.CuspFormClass.eichlerIntegral_slash_apply_of_mem: the transformation law for σ in the level of f.
• TauCeti.CuspFormClass.eichlerIntegral_slash_eq_of_cuspIntegral_eq_zero: if the periods ∫_{σ⁻¹ • ∞}^{i∞} f(z) zʲ dz, j ≤ n, vanish, then E_f ∣[-n] σ = E_f.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, §8.2.
• M. Eichler, Eine Verallgemeinerung der Abelschen Integrale, Math. Z. 67 (1957), 267–298.
• The AINTLIB LeanModularForms project, ModularSymbols/EichlerInjective.lean (eichler_slash_invariant), where the transformation law is proved for the q-expansion Eichler integral.

theorem TauCeti.CuspFormClass.eichlerIntegral_slash_apply {Γ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} {n : ℕ} {h : ℝ} [Γ.IsArithmetic] [CuspFormClass F Γ k] (hk : k = ↑n + 2) (f : F) (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {Γ' : Subgroup (GL (Fin 2) ℝ)} {F' : Type u_2} [FunLike F' UpperHalfPlane ℂ] [CuspFormClass F' Γ' k] (f' : F') {h' : ℝ} (hh' : 0 < h') (hΓ' : h' ∈ Γ'.strictPeriods) (σ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (hf' : ⇑f' = SlashAction.map k σ ⇑f) (τ : UpperHalfPlane) : SlashAction.map (-↑n) σ (eichlerIntegral h (n + 1) ⇑f) τ = eichlerIntegral h' (n + 1) (⇑f') τ - (-2 * ↑Real.pi * Complex.I) ^ (n + 1) / ↑n.factorial * cuspIntegral (fun (z : UpperHalfPlane) => f' z * (↑z - ↑τ) ^ n) ((Matrix.SpecialLinearGroup.mapGL ℚ) σ⁻¹ • OnePoint.infty) OnePoint.infty

The transformation law of the Eichler integral. Let f be a cusp form of weight k = n + 2 on an arithmetic subgroup, σ ∈ SL(2, ℤ), and f' a cusp form (for any subgroup with a positive strict period h') with f' = f ∣[k] σ. Then the Eichler integrals E_f = E_{n+1} f and E_{f'} satisfy

(E_f ∣[-n] σ)(τ) = E_{f'}(τ) - (-2πi)ⁿ⁺¹ / n! · ∫_{σ⁻¹ • ∞}^{i∞} f'(z) (z - τ)ⁿ dz,

the integral taken along the geodesic between the two cusps. By TauCeti.ModularSymbols.cuspIntegral_mul_sub_pow the correction term is a polynomial in τ of degree at most n whose coefficients are periods of f'.

theorem TauCeti.CuspFormClass.eichlerIntegral_slash_apply_of_mem {Γ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} {n : ℕ} {h : ℝ} [Γ.IsArithmetic] [CuspFormClass F Γ k] (hk : k = ↑n + 2) (f : F) (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {σ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hσ : (Matrix.SpecialLinearGroup.mapGL ℝ) σ ∈ Γ) (τ : UpperHalfPlane) : SlashAction.map (-↑n) σ (eichlerIntegral h (n + 1) ⇑f) τ = eichlerIntegral h (n + 1) (⇑f) τ - (-2 * ↑Real.pi * Complex.I) ^ (n + 1) / ↑n.factorial * cuspIntegral (fun (z : UpperHalfPlane) => f z * (↑z - ↑τ) ^ n) ((Matrix.SpecialLinearGroup.mapGL ℚ) σ⁻¹ • OnePoint.infty) OnePoint.infty

The transformation law of the Eichler integral in the level. For a cusp form f of weight k = n + 2 on an arithmetic subgroup Γ and σ ∈ SL(2, ℤ) with σ ∈ Γ, the Eichler integral E_f = E_{n+1} f transforms in weight -n up to the period polynomial of f at σ:

(E_f ∣[-n] σ)(τ) = E_f(τ) - (-2πi)ⁿ⁺¹ / n! · ∫_{σ⁻¹ • ∞}^{i∞} f(z) (z - τ)ⁿ dz.

theorem TauCeti.CuspFormClass.eichlerIntegral_slash_eq_of_cuspIntegral_eq_zero {Γ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} {n : ℕ} {h : ℝ} [Γ.IsArithmetic] [CuspFormClass F Γ k] (hk : k = ↑n + 2) (f : F) (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {σ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hσ : (Matrix.SpecialLinearGroup.mapGL ℝ) σ ∈ Γ) (hper : ∀ j ≤ n, cuspIntegral (fun (z : UpperHalfPlane) => f z * ↑z ^ j) ((Matrix.SpecialLinearGroup.mapGL ℚ) σ⁻¹ • OnePoint.infty) OnePoint.infty = 0) : SlashAction.map (-↑n) σ (eichlerIntegral h (n + 1) ⇑f) = eichlerIntegral h (n + 1) ⇑f

Vanishing periods make the Eichler integral invariant. For a cusp form f of weight k = n + 2 on an arithmetic subgroup Γ and σ ∈ SL(2, ℤ) with σ ∈ Γ, if the periods ∫_{σ⁻¹ • ∞}^{i∞} f(z) zʲ dz vanish for j ≤ n, then the Eichler integral E_f = E_{n+1} f is invariant under σ in weight -n: E_f ∣[-n] σ = E_f.