Documentation

TauCeti.NumberTheory.ModularForms.LFunction.Period

Periods of cusp forms are values of their L-functions #

Let f be a cusp form of weight k > 0 on an arithmetic subgroup Γ. Its periods are the integrals rₙ(f) = ∫₀^{i∞} f(τ) τⁿ dτ, n ≥ 0, along the positive imaginary axis, the integral TauCeti.cuspIntegral between the cusps 0 and ∞. Substituting τ = i t turns rₙ(f) into iⁿ⁺¹ times the Mellin transform of t ↦ f(i t) at n + 1, which is Mathlib's completed L-function ModularForm.Λ:

rₙ(f) = iⁿ⁺¹ Λ(f, n + 1) = n! / (-2πi)ⁿ⁺¹ · L(f, n + 1).

For f of weight k = w + 2 and 0 ≤ n ≤ w these are the values of L(f, s) at the critical integers s = 1, …, k - 1, and they are, up to binomial coefficients and signs, the coefficients of the period polynomial of f. This is how nonvanishing of L-values enters the Eichler–Shimura theory of period polynomials.

Main results #

References #

theorem TauCeti.cuspIntegral_mul_pow_zero_infty {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [CuspFormClass F Γ k] (hk : 0 < k) (f : F) (n : ℕ) :
cuspIntegral (fun (τ : UpperHalfPlane) => f τ * ↑τ ^ n) (↑0) OnePoint.infty = Complex.I ^ (n + 1) * ModularForm.Λ hk f (↑n + 1)

Periods are completed L-values: the period ∫₀^{i∞} f(τ) τⁿ dτ of a cusp form f of positive weight on an arithmetic subgroup is iⁿ⁺¹ Λ(f, n + 1), for Mathlib's completed L-function ModularForm.Λ.

theorem TauCeti.cuspIntegral_mul_pow_zero_infty_eq_L {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [CuspFormClass F Γ k] (hk : 0 < k) (f : F) (n : ℕ) :
cuspIntegral (fun (τ : UpperHalfPlane) => f τ * ↑τ ^ n) (↑0) OnePoint.infty = ↑n.factorial / (-2 * ↑Real.pi * Complex.I) ^ (n + 1) * ModularForm.L hk f (↑n + 1)

Periods are L-values at positive integers: the period ∫₀^{i∞} f(τ) τⁿ dτ of a cusp form f of positive weight k on an arithmetic subgroup is n! / (-2πi)ⁿ⁺¹ · L(f, n + 1), for Mathlib's L-function ModularForm.L. For 0 ≤ n ≤ k - 2 these are the critical values.