Nonvanishing of Galois character series on the line Re s = 1

Let F / K be a finite Galois extension of number fields and χ a character of Gal(F/K). On Re s > 1 the L-series of galoisCharacterWeight χ does not vanish, by its Euler product. This file gives criteria for a function agreeing on Re s > 1 with the L-series of galoisCharacterWeight χ to be nonzero at a point s of the line Re s = 1. In particular the series of the trivial character, which is the Dedekind zeta function of K with the Euler factors at the primes ramified in F deleted, does not vanish at any s ≠ 1 with Re s = 1.

Together with the continuation across Re s = 1, this is what makes the logarithmic derivatives of these series, with the pole of the trivial one subtracted, continuous on Re s ≥ 1: the boundary behaviour required to apply a Tauberian theorem to the Frobenius von Mangoldt series.

The criterion is the 3-4-1 criterion TauCeti.UnitaryIdealWeight.ne_zero_of_eqOn_LSeries for the unitary weight galoisCharacterUnitaryWeight χ, whose pointwise square is the unitary weight of χ². The remaining results handle the square: for χ² = 1 its series is the trivial one, which continues across Re s = 1 away from s = 1 by TauCeti.exists_differentiableOn_eq_LSeries_ofBadPrimes_sub.

Main results

• MonoidHom.LSeries_galoisCharacterWeight_ne_zero: the series of χ is nonzero on Re s > 1.
• NumberField.Chebotarev.ne_zero_of_eqOn_LSeries_galoisCharacterWeight: a continuation of the series of χ, differentiable at s = 1 + it, is nonzero at s provided some continuation of the series of χ² is continuous at 1 + 2it.
• NumberField.Chebotarev.ne_zero_of_eqOn_LSeries_galoisCharacterWeight_of_sq_eq_one: for χ² = 1, a continuation of the series of χ is nonzero on Re s = 1 away from s = 1.
• NumberField.Chebotarev.ne_zero_of_eqOn_LSeries_galoisCharacterWeight_one: a continuation of the trivial-character series is nonzero on Re s = 1 away from s = 1.
• NumberField.Chebotarev.exists_continuousOn_eq_neg_logDeriv_galoisCharacterWeight_one_sub: the regularized logarithmic derivative of the trivial character extends continuously to Re s ≥ 1.

References

• H. Davenport, Multiplicative Number Theory, Chapter 4.
• The case analysis on χ² 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 MonoidHom.LSeries_galoisCharacterWeight_ne_zero {K : Type u_1} {F : Type u_2} [Field K] [NumberField K] [Field F] [NumberField F] [Algebra K F] [IsGalois K F] (χ : Gal(F/K) →* ℂˣ) {s : ℂ} (hs : 1 < s.re) : LSeries (⇑((TauCeti.normCoeff K) χ.galoisCharacterWeight.toIdealArithmeticFunction)) s ≠ 0

Nonvanishing on Re s > 1. For a finite Galois extension F / K and a character χ of Gal(F/K), the L-series of galoisCharacterWeight χ is nonzero at every s with 1 < Re s, where its Euler product converges absolutely.

theorem NumberField.Chebotarev.ne_zero_of_eqOn_LSeries_galoisCharacterWeight {K : Type u_1} {F : Type u_2} [Field K] [NumberField K] [Field F] [NumberField F] [Algebra K F] [IsGalois K F] (χ : Gal(F/K) →* ℂˣ) {s : ℂ} (hs : s.re = 1) {f f₂ : ℂ → ℂ} (hf : DifferentiableAt ℂ f s) (hfL : Set.EqOn f (LSeries ⇑((TauCeti.normCoeff K) χ.galoisCharacterWeight.toIdealArithmeticFunction)) {z : ℂ | 1 < z.re}) (hf₂ : ContinuousAt f₂ (2 * s - 1)) (hf₂L : Set.EqOn f₂ (LSeries ⇑((TauCeti.normCoeff K) (χ ^ 2).galoisCharacterWeight.toIdealArithmeticFunction)) {z : ℂ | 1 < z.re}) : f s ≠ 0

The 3-4-1 criterion for a Galois character. Let F / K be a finite Galois extension, χ a character of Gal(F/K), and s = 1 + it. If f is complex differentiable at s and f₂ is continuous at 1 + 2it = 2s - 1, and they agree on Re s > 1 with the L-series of χ and of χ² respectively, then f s ≠ 0.

theorem NumberField.Chebotarev.ne_zero_of_eqOn_LSeries_galoisCharacterWeight_of_sq_eq_one {K : Type u_1} {F : Type u_2} [Field K] [NumberField K] [Field F] [NumberField F] [Algebra K F] [IsGalois K F] (χ : Gal(F/K) →* ℂˣ) (hχ : χ ^ 2 = 1) {f : ℂ → ℂ} {s : ℂ} (hs : s.re = 1) (hs1 : s ≠ 1) (hf : DifferentiableAt ℂ f s) (hfL : Set.EqOn f (LSeries ⇑((TauCeti.normCoeff K) χ.galoisCharacterWeight.toIdealArithmeticFunction)) {z : ℂ | 1 < z.re}) : f s ≠ 0

Nonvanishing on Re s = 1 for a character of order at most two. Let F / K be a finite Galois extension and χ a character of Gal(F/K) with χ² = 1. If f agrees on Re s > 1 with the L-series of χ and is complex differentiable at a point s ≠ 1 with Re s = 1, then f s ≠ 0.

theorem NumberField.Chebotarev.ne_zero_of_eqOn_LSeries_galoisCharacterWeight_one {K : Type u_1} {F : Type u_2} [Field K] [NumberField K] [Field F] [NumberField F] [Algebra K F] [IsGalois K F] {f : ℂ → ℂ} {s : ℂ} (hs : s.re = 1) (hs1 : s ≠ 1) (hf : DifferentiableAt ℂ f s) (hfL : Set.EqOn f (LSeries ⇑((TauCeti.normCoeff K) (MonoidHom.galoisCharacterWeight 1).toIdealArithmeticFunction)) {z : ℂ | 1 < z.re}) : f s ≠ 0

The trivial-character series has no zeros on Re s = 1 except at the pole. Let F / K be a finite Galois extension. If f agrees on Re s > 1 with the L-series of the trivial character of Gal(F/K), which is the Dedekind zeta function of K with the Euler factors at the ramified primes deleted, and f is complex differentiable at a point s ≠ 1 with Re s = 1, then f s ≠ 0.

theorem NumberField.Chebotarev.exists_continuousOn_eq_neg_logDeriv_galoisCharacterWeight_one_sub (K : Type u_1) (F : Type u_2) [Field K] [NumberField K] [Field F] [NumberField F] [Algebra K F] [IsGalois K F] : ∃ (G : ℂ → ℂ), ContinuousOn G {s : ℂ | 1 ≤ s.re} ∧ ∀ (s : ℂ), 1 < s.re → G s = -logDeriv (LSeries ⇑((TauCeti.normCoeff K) (MonoidHom.galoisCharacterWeight 1).toIdealArithmeticFunction)) s - 1 / (s - 1)

The regularized boundary function of the trivial character. Let F / K be a finite Galois extension and L_1 the L-series of the trivial character of Gal(F/K), that is the Dedekind zeta function of K with the Euler factors at the primes ramified in F deleted. Then -L_1'(s) / L_1(s) - 1 / (s - 1) extends from Re s > 1 to a function continuous on Re s ≥ 1.