The continued L-series of a cyclotomic Galois character

For a finite Galois extension F / K of number fields and a character χ of Gal(F/K), cyclotomicCharacterSeriesC K F χ is a holomorphic continuation of the L-series of the ideal weight galoisCharacterWeight χ to the half-plane Re s > 1 - 1 / [K : ℚ] when one exists, and the L-series itself otherwise. For every χ it agrees with the L-series on Re s > 1.

For a cyclotomic extension F = K(μ_m) and a nontrivial character χ, the continuation exists, so the series is analytic at s = 1, and its value at s = 1 is nonzero. For the trivial character the series is the Dedekind zeta function of K with the Euler factors at the ramified primes deleted, which continues across Re s = 1 apart from a single simple pole at s = 1.

Main definitions

• NumberField.Chebotarev.cyclotomicCharacterSeriesC: the continued L-series of a Galois character.

Main results

• NumberField.Chebotarev.cyclotomicCharacterSeriesC_eq_LSeries: on Re s > 1 it is the L-series of galoisCharacterWeight χ.
• NumberField.Chebotarev.logDeriv_cyclotomicCharacterSeriesC: the logarithmic derivative agrees with that of the character L-series on Re s > 1.
• NumberField.Chebotarev.differentiableOn_cyclotomicCharacterSeriesC: for F = K(μ_m) and χ nontrivial it is holomorphic on Re s > 1 - 1 / [K : ℚ].
• NumberField.Chebotarev.analyticAt_cyclotomicCharacterSeriesC_one: for F = K(μ_m) and χ nontrivial it is analytic at s = 1.
• NumberField.Chebotarev.cyclotomicCharacterSeriesC_ne_zero_at_one: for F = K(μ_m) and χ nontrivial it is nonzero at s = 1.

References

• The nonvanishing argument at s = 1, in which the logarithm of the product of the L-series over all characters is a series with nonnegative coefficients that is unbounded as s → 1⁺, is analogous to Chebotarev.artinLSeries_one_ne_zero in AINTLIB (github.com/CBirkbeck/aintlib at commit 8102fa09bbf570f3e991adfdb2d6d70b48cb5b5e, Apache-2.0), projects/Chebotarev/CebotarevDensity/ZetaProduct.lean, which proves the nonvanishing at s = 1 of the Artin L-series of a nontrivial character of Gal(K(μ_m)/K).

noncomputable def NumberField.Chebotarev.cyclotomicCharacterSeriesC (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) →* ℂˣ) : ℂ → ℂ

The continued L-series of a Galois character. If the L-series of galoisCharacterWeight χ has a holomorphic continuation from Re s > 1 to the half-plane Re s > 1 - 1 / [K : ℚ], this is a choice of one; otherwise it is the L-series itself.

In every case it is the L-series on Re s > 1 (cyclotomicCharacterSeriesC_eq_LSeries). For F = K(μ_m) and χ ≠ 1 the continuation exists, and the function is analytic and nonzero at s = 1 (analyticAt_cyclotomicCharacterSeriesC_one, cyclotomicCharacterSeriesC_ne_zero_at_one).

@[simp]

theorem NumberField.Chebotarev.cyclotomicCharacterSeriesC_eq_LSeries (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) : cyclotomicCharacterSeriesC K F χ s = LSeries (⇑((TauCeti.normCoeff K) χ.galoisCharacterWeight.toIdealArithmeticFunction)) s

The continued L-series is the L-series on Re s > 1. This holds for every Galois extension F / K and every character χ, with no cyclotomic hypothesis.

theorem NumberField.Chebotarev.logDeriv_cyclotomicCharacterSeriesC (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) : logDeriv (cyclotomicCharacterSeriesC K F χ) s = logDeriv (LSeries ⇑((TauCeti.normCoeff K) χ.galoisCharacterWeight.toIdealArithmeticFunction)) s

The logarithmic derivative on Re s > 1. For every finite Galois extension F / K and every character χ of Gal(F/K), the logarithmic derivative of the continued series cyclotomicCharacterSeriesC K F χ is that of the L-series of galoisCharacterWeight χ on Re s > 1, where the two functions agree on a neighbourhood.

theorem NumberField.Chebotarev.differentiableOn_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) : DifferentiableOn ℂ (cyclotomicCharacterSeriesC K F χ) {s : ℂ | 1 - 1 / ↑(Module.finrank ℚ K) < s.re}

Holomorphy on Re s > 1 - 1 / [K : ℚ]. For F = K(μ_m) and a nontrivial character χ of Gal(F/K), the continued L-series of χ is holomorphic on the half-plane Re s > 1 - 1 / [K : ℚ].

theorem NumberField.Chebotarev.analyticAt_cyclotomicCharacterSeriesC_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) : AnalyticAt ℂ (cyclotomicCharacterSeriesC K F χ) 1

Analyticity at s = 1. For F = K(μ_m) and a nontrivial character χ of Gal(F/K), the continued L-series of χ is analytic at s = 1, which lies in the half-plane of differentiableOn_cyclotomicCharacterSeriesC.

theorem NumberField.Chebotarev.cyclotomicCharacterSeriesC_ne_zero_at_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) : cyclotomicCharacterSeriesC K F χ 1 ≠ 0

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