Nonvanishing of L-functions on the level-one newform basis

At level one, the canonical Hecke eigenbasis TauCeti.levelOneNewformBasis k of CuspForm 𝒮ℒ k transports each f : Newform 1 k along (Gamma1 1).map (mapGL ℝ) = 𝒮ℒ without changing the underlying function on ℍ, and the cusp at ∞ has strict width 1. Consequently, on the Euler-product half-plane Re s > k / 2 + 1, Mathlib's ModularForm.L of levelOneNewformBasis k f coincides with the q-expansion LSeries of f.toCuspForm and therefore does not vanish.

Main results

• TauCeti.L_levelOneNewformBasis_ne_zero: for 0 < k, f : Newform 1 k, and (k : ℝ) / 2 + 1 < s.re, ModularForm.L hk (levelOneNewformBasis k f) s ≠ 0.

References

• F. Diamond and J. Shurman, A first course in modular forms, Proposition 5.8.5 and §5.9.

theorem TauCeti.L_levelOneNewformBasis_ne_zero {k : ℤ} (hk : 0 < k) (f : HeckeRing.GL2.Newform 1 k) {s : ℂ} (hs : ↑k / 2 + 1 < s.re) : ModularForm.L hk ((levelOneNewformBasis k) f) s ≠ 0

On the Euler-product half-plane Re s > k / 2 + 1, ModularForm.L of the level-one newform basis vector levelOneNewformBasis k f does not vanish.