Evaluating logarithmic-derivative coefficients of ideal Euler factors

For a general ideal Euler product, the formal series TauCeti.EulerProductData.localLogDerivSeries records the prime-power coefficients of the logarithmic derivative of each local factor. This file evaluates those formal coefficients at N(P) ^ (-s) and identifies their sum with the analytic logarithmic derivative at s.

Two hypotheses are visible in the result. The coefficient series must converge at the evaluation point, and the local Euler factor must be nonzero there. These cannot be replaced by convergence of the local factor itself: a convergent power series can have a zero closer to the origin than the point being evaluated, in which case its formal logarithmic derivative does not converge at that point.

The local identity is also combined with the prime-indexed logarithmic-derivative sum. Thus, once coefficient convergence is known at every prime, the logarithmic derivative of the global L-series is the sum of the evaluated local formal series.

Main results

• TauCeti.EulerProductData.localPowerSeries_eval_eq_eulerFactor: evaluation of the local power series at N(P) ^ (-s).
• TauCeti.EulerProductData.logDeriv_eulerFactor_eq_neg_log_mul_tsum_coeff_localLogDerivSeries: evaluation of one local formal logarithmic derivative.
• TauCeti.EulerProductData.hasSum_tsum_coeff_localLogDerivSeries: the corresponding expansion of the logarithmic derivative of the global L-series.

References

• J. Neukirch, Algebraic Number Theory, Chapter VII.
• G. Tenenbaum, Introduction to Analytic and Probabilistic Number Theory, Chapter I.2.

@[simp]

theorem TauCeti.EulerProductData.localPowerSeries_eval_eq_eulerFactor {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (s : ℂ) : FormalMultilinearSeries.ofScalarsSum (fun (n : ℕ) => D.toIdealArithmeticFunction (P.primeIdealPow n)) (↑(Ideal.absNorm P.asIdeal) ^ (-s)) = D.eulerFactor P s

Evaluating the local power series at N(P) ^ (-s) gives the local Euler factor at s.

theorem TauCeti.EulerProductData.eulerFactor_ne_zero_of_localPowerSeries_ne_zero {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) {s : ℂ} (hne : FormalMultilinearSeries.ofScalarsSum (fun (n : ℕ) => (PowerSeries.coeff n) (D.localPowerSeries P)) (↑(Ideal.absNorm P.asIdeal) ^ (-s)) ≠ 0) : D.eulerFactor P s ≠ 0

A local Euler factor is nonzero at s if the corresponding local power series is nonzero at N(P) ^ (-s).

theorem TauCeti.EulerProductData.logDeriv_eulerFactor_eq_neg_log_mul_tsum_coeff_localLogDerivSeries {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) {s : ℂ} (hs : LSeries.abscissaOfAbsConv ⇑(D.localArithmeticFactor P) < ↑s.re) (hne : D.eulerFactor P s ≠ 0) (hcoeff : Summable fun (e : ℕ) => (PowerSeries.coeff e) (D.localLogDerivSeries P) * (↑(Ideal.absNorm P.asIdeal) ^ (-s)) ^ e) : logDeriv (D.eulerFactor P) s = -Complex.log ↑(Ideal.absNorm P.asIdeal) * ∑' (e : ℕ), (PowerSeries.coeff e) (D.localLogDerivSeries P) * (↑(Ideal.absNorm P.asIdeal) ^ (-s)) ^ e

Evaluation of a local formal logarithmic derivative. If the coefficient series of X F_P'(X) / F_P(X) converges at X = N(P) ^ (-s) and the local Euler factor does not vanish at s, then the analytic logarithmic derivative is -log N(P) times that sum.

The explicit convergence hypothesis is necessary: convergence and nonvanishing of F_P at one point do not imply convergence there of the Taylor series of F_P'/F_P about zero.

theorem TauCeti.EulerProductData.hasSum_tsum_coeff_localLogDerivSeries {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) {s : ℂ} (hs : idealAbscissaOfAbsConv K D.toIdealArithmeticFunction < ↑s.re) (hne : ∀ (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), D.eulerFactor P s ≠ 0) (hcoeff : ∀ (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), Summable fun (e : ℕ) => (PowerSeries.coeff e) (D.localLogDerivSeries P) * (↑(Ideal.absNorm P.asIdeal) ^ (-s)) ^ e) : HasSum (fun (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => -Complex.log ↑(Ideal.absNorm P.asIdeal) * ∑' (e : ℕ), (PowerSeries.coeff e) (D.localLogDerivSeries P) * (↑(Ideal.absNorm P.asIdeal) ^ (-s)) ^ e) (logDeriv (LSeries ⇑((normCoeff K) D.toIdealArithmeticFunction)) s)

The logarithmic derivative of a general ideal Euler product, expanded in its local formal coefficients. If every local formal logarithmic-derivative series converges at N(P) ^ (-s), the global logarithmic derivative is the sum of their evaluations weighted by -log N(P).

theorem TauCeti.EulerProductData.logDeriv_LSeries_eq_tsum_tsum_coeff_localLogDerivSeries {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) {s : ℂ} (hs : idealAbscissaOfAbsConv K D.toIdealArithmeticFunction < ↑s.re) (hne : ∀ (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), D.eulerFactor P s ≠ 0) (hcoeff : ∀ (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), Summable fun (e : ℕ) => (PowerSeries.coeff e) (D.localLogDerivSeries P) * (↑(Ideal.absNorm P.asIdeal) ^ (-s)) ^ e) : logDeriv (LSeries ⇑((normCoeff K) D.toIdealArithmeticFunction)) s = ∑' (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), -Complex.log ↑(Ideal.absNorm P.asIdeal) * ∑' (e : ℕ), (PowerSeries.coeff e) (D.localLogDerivSeries P) * (↑(Ideal.absNorm P.asIdeal) ^ (-s)) ^ e

The tsum form of TauCeti.EulerProductData.hasSum_tsum_coeff_localLogDerivSeries.