The Eichler integral as an integral

The (n + 1)-fold Eichler integral E_{n+1} f = ∑ (h / m)ⁿ⁺¹ aₘ qᵐ of TauCeti.NumberTheory.ModularForms.EichlerIntegral.Basic is defined by its q-expansion. When the constant term a₀ of f vanishes, it is also the integral

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

along the vertical ray from τ to i∞, parametrized as z = τ + i t for t > 0. Along the ray qᵐ decays like e^{-2πmt/h}, so termwise this is the Gamma integral ∫₀^∞ tⁿ e^{-ct} dt = n! / cⁿ⁺¹ at c = 2πm / h.

For a cusp form f of weight k = n + 2, the integrand f(z) (z - τ)ⁿ dz is the period integrand of f against the binary form (X - τY)ⁿ, so this representation ties the Eichler integral to the periods of f. It is one input to the transformation law: E_{k-1} f transforms in weight 2 - k up to a polynomial in τ of degree at most k - 2 whose coefficients are periods of f. Proving that law also needs the substitution z ↦ γz in this integral and path independence for integrals from a point of ℍ to a cusp, since γ moves the vertical ray to a path with different endpoints. Neither is part of this file.

Main results

• TauCeti.eichlerIntegral_eq_integral: the integral representation, for a holomorphic periodic function bounded at i∞ with vanishing constant term.
• TauCeti.CuspFormClass.eichlerIntegral_eq_integral: the integral representation for a cusp form.
• TauCeti.integrableOn_eichlerIntegrand, TauCeti.CuspFormClass.integrableOn_eichlerIntegrand: the integrand is integrable along the ray, under the same hypotheses.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, §8.2.
• W. Kohnen, D. Zagier, Modular forms with rational periods, in Modular forms (Durham, 1983), Ellis Horwood, 1984, 197–249.

theorem TauCeti.integrableOn_eichlerIntegrand {h : ℝ} {f : UpperHalfPlane → ℂ} (hh : 0 < h) (hfper : Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) ↑h) (hfhol : MDiff f) (hfbdd : UpperHalfPlane.IsBoundedAtImInfty f) (h₀ : (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion h f) = 0) (n : ℕ) (τ : UpperHalfPlane) : MeasureTheory.IntegrableOn (fun (t : ℝ) => f (↑UpperHalfPlane.ofComplex (↑τ + ↑t * Complex.I)) * (↑t * Complex.I) ^ n * Complex.I) (Set.Ioi 0) MeasureTheory.volume

If f is holomorphic, h-periodic and bounded at i∞ with vanishing constant term a₀, then the period integrand f(z) (z - τ)ⁿ dz is integrable along the vertical ray z = τ + i t, t > 0.

theorem TauCeti.eichlerIntegral_eq_integral {h : ℝ} {f : UpperHalfPlane → ℂ} (hh : 0 < h) (hfper : Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) ↑h) (hfhol : MDiff f) (hfbdd : UpperHalfPlane.IsBoundedAtImInfty f) (h₀ : (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion h f) = 0) (n : ℕ) (τ : UpperHalfPlane) : eichlerIntegral h (n + 1) f τ = (-2 * ↑Real.pi * Complex.I) ^ (n + 1) / ↑n.factorial * ∫ (t : ℝ) in Set.Ioi 0, f (↑UpperHalfPlane.ofComplex (↑τ + ↑t * Complex.I)) * (↑t * Complex.I) ^ n * Complex.I

The Eichler integral as an integral: if f is holomorphic, h-periodic and bounded at i∞ with vanishing constant term a₀, then

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

the integral taken along the vertical ray z = τ + i t, t > 0. The integrand is integrable by TauCeti.integrableOn_eichlerIntegrand.

theorem TauCeti.CuspFormClass.integrableOn_eichlerIntegrand {h : ℝ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [CuspFormClass F Γ k] (f : F) (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (n : ℕ) (τ : UpperHalfPlane) : MeasureTheory.IntegrableOn (fun (t : ℝ) => f (↑UpperHalfPlane.ofComplex (↑τ + ↑t * Complex.I)) * (↑t * Complex.I) ^ n * Complex.I) (Set.Ioi 0) MeasureTheory.volume

For a cusp form f, the period integrand f(z) (z - τ)ⁿ dz is integrable along the vertical ray z = τ + i t, t > 0.

theorem TauCeti.CuspFormClass.eichlerIntegral_eq_integral {h : ℝ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [CuspFormClass F Γ k] (f : F) (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (n : ℕ) (τ : UpperHalfPlane) : eichlerIntegral h (n + 1) (⇑f) τ = (-2 * ↑Real.pi * Complex.I) ^ (n + 1) / ↑n.factorial * ∫ (t : ℝ) in Set.Ioi 0, f (↑UpperHalfPlane.ofComplex (↑τ + ↑t * Complex.I)) * (↑t * Complex.I) ^ n * Complex.I

The Eichler integral of a cusp form as an integral: for a cusp form f,

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

the integral taken along the vertical ray z = τ + i t, t > 0. For a cusp form of weight k ≥ 2 and n = k - 2, this is the classical integral formula for its Eichler integral.