The continued L-function of a cancelling weight does not vanish on Re s ≥ 1

Let χ be a unitary ideal weight of a number field K with cancellation (TauCeti.HasCancellation χ), so that its continued L-function TauCeti.continuedLFunctionOfWeight χ is holomorphic on Re s > 1 - 1 / [K : ℚ]. On Re s > 1 it is the L-series of χ, which does not vanish there because of its Euler product. This file proves that it has no zeros on the line Re s = 1 either, under a hypothesis on the pointwise square χ ^ 2.

The classical 3-4-1 argument compares χ with χ ^ 2: for σ > 1, 1 ≤ ‖ζ_K(σ) ^ 3 L(χ, σ + it) ^ 4 L(χ ^ 2, σ + 2it)‖. A zero of L(χ, ·) at 1 + it outweighs the simple pole of ζ_K at 1, provided the L-series of χ ^ 2 continues continuously to 1 + 2it (TauCeti.UnitaryIdealWeight.ne_zero_of_eqOn_LSeries). The square is handled in two ways:

• if χ ^ 2 also has cancellation, its own continued L-function supplies the continuation, and the continued L-function of χ has no zero on Re s ≥ 1;
• if χ ^ 2 is a norm twist I ↦ N(I) ^ (u * I) on its good ideals (as for a quadratic character, where u = 0), its L-series is a translate of a Dedekind zeta function with finitely many Euler factors deleted. That translate is continuous away from its pole at 1 + u * I, which leaves only the point s = 1 + (u / 2) * I uncovered.

The cases are not exhaustive in general. A character-family argument supplies cancellation for the nondegenerate members of its family. For a quadratic character the excluded point s = 1 needs a different argument, since there L(χ ^ 2, ·) has a pole.

Main results

• TauCeti.continuedLFunctionOfWeight_ne_zero_of_one_lt_re: nonvanishing on Re s > 1, for every unitary weight.
• TauCeti.continuedLFunctionOfWeight_ne_zero_of_hasCancellation_sq: if both χ and χ ^ 2 have cancellation, the continued L-function of χ has no zeros on Re s ≥ 1.
• TauCeti.continuedLFunctionOfWeight_ne_zero_of_isNormTwistOnGood_sq: if χ has cancellation and χ ^ 2 is a norm twist with parameter u on its good ideals, there are no zeros on Re s ≥ 1 other than possibly 1 + (u / 2) * I.
• TauCeti.continuedLFunctionOfWeight_ne_zero_of_isTrivialOnGood_sq: the case u = 0, for weights whose square is trivial on its good ideals.

References

• H. Davenport, Multiplicative Number Theory, Chapter 4.
• The case analysis on the square follows Mathlib's Mathlib/NumberTheory/LSeries/Nonvanishing.lean (Michael Stoll and David Loeffler), where DirichletCharacter.LFunction_ne_zero_of_re_eq_one proves the analogous statement for Dirichlet L-functions.

theorem TauCeti.continuedLFunctionOfWeight_ne_zero_of_one_lt_re {K : Type u_1} [Field K] [NumberField K] (χ : UnitaryIdealWeight K) {s : ℂ} (hs : 1 < s.re) : continuedLFunctionOfWeight χ s ≠ 0

No zeros to the right of 1. For every unitary weight χ, with or without cancellation, the continued L-function of χ does not vanish on Re s > 1: there it is the L-series of χ, an absolutely convergent Euler product.

theorem TauCeti.continuedLFunctionOfWeight_ne_zero_of_hasCancellation_sq {K : Type u_1} [Field K] [NumberField K] {χ : UnitaryIdealWeight K} (hχ : HasCancellation χ) (hχ₂ : HasCancellation (χ ^ 2)) {s : ℂ} (hs : 1 ≤ s.re) : continuedLFunctionOfWeight χ s ≠ 0

Nonvanishing when the square also cancels. If a unitary weight χ and its pointwise square χ ^ 2 both have cancellation, the continued L-function of χ has no zeros on the closed half-plane Re s ≥ 1.

theorem TauCeti.continuedLFunctionOfWeight_ne_zero_of_isNormTwistOnGood_sq {K : Type u_1} [Field K] [NumberField K] {χ : UnitaryIdealWeight K} (hχ : HasCancellation χ) {u : ℝ} (hχ₂ : (↑(χ ^ 2)).IsNormTwistOnGood u) {s : ℂ} (hs : 1 ≤ s.re) (hsu : s ≠ 1 + ↑u / 2 * Complex.I) : continuedLFunctionOfWeight χ s ≠ 0

Nonvanishing when the square is a norm twist on its good ideals. Let χ be a unitary weight with cancellation whose pointwise square agrees with I ↦ N(I) ^ (u * I) on its good ideals. Then the continued L-function of χ has no zeros on Re s ≥ 1 except possibly at s = 1 + (u / 2) * I, where the L-series of χ ^ 2 has its pole at 2s - 1 = 1 + u * I.

theorem TauCeti.continuedLFunctionOfWeight_ne_zero_of_isTrivialOnGood_sq {K : Type u_1} [Field K] [NumberField K] {χ : UnitaryIdealWeight K} (hχ : HasCancellation χ) (hχ₂ : (↑(χ ^ 2)).IsTrivialOnGood) {s : ℂ} (hs : 1 ≤ s.re) (hs1 : s ≠ 1) : continuedLFunctionOfWeight χ s ≠ 0

Nonvanishing when the square is trivial on its good ideals, as for a quadratic character. If a unitary weight χ has cancellation and χ ^ 2 takes the value 1 on its good ideals, the continued L-function of χ has no zeros on Re s ≥ 1 except possibly at s = 1.