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

For a cyclotomic extension F = K(μ_m) of a number field K and a nontrivial character χ of Gal(F/K), the continued L-series cyclotomicCharacterSeriesC K F χ does not vanish anywhere on the line Re s = 1. The series of the trivial character, which has a pole at s = 1, is treated for every finite Galois extension in TauCeti.NumberTheory.Chebotarev.GaloisCharacter.Nonvanishing.

Main results

• NumberField.Chebotarev.cyclotomicCharacterSeriesC_ne_zero_of_re_eq_one: for F = K(μ_m) and χ ≠ 1, the continued series of χ is nonzero on Re s = 1.
• NumberField.Chebotarev.continuousOn_logDeriv_cyclotomicCharacterSeriesC: for nontrivial characters, the logarithmic derivative is continuous on 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 NumberField.Chebotarev.cyclotomicCharacterSeriesC_ne_zero_of_re_eq_one {K : Type u_1} {F : Type u_2} [Field K] [NumberField K] [Field F] [NumberField F] [Algebra K F] [IsGalois K F] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} K F] (χ : Gal(F/K) →* ℂˣ) (hχ : χ ≠ 1) {s : ℂ} (hs : s.re = 1) : cyclotomicCharacterSeriesC K F χ s ≠ 0

Nonvanishing on Re s = 1. For F = K(μ_m) and a nontrivial character χ of Gal(F/K), the continued L-series of χ does not vanish at any s with Re s = 1.

theorem NumberField.Chebotarev.continuousOn_logDeriv_cyclotomicCharacterSeriesC (K : Type u_1) (F : Type u_2) [Field K] [NumberField K] [Field F] [NumberField F] [Algebra K F] [IsGalois K F] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} K F] (χ : Gal(F/K) →* ℂˣ) (hχ : χ ≠ 1) : ContinuousOn (logDeriv (cyclotomicCharacterSeriesC K F χ)) {s : ℂ | 1 ≤ s.re}

Continuity of the logarithmic derivative on Re s ≥ 1. For F = K(μ_m) and a nontrivial character χ of Gal(F/K), the logarithmic derivative of the continued series of χ is continuous on the closed half-plane Re s ≥ 1: the series is holomorphic on a neighbourhood of it and does not vanish on it.