The logarithmic derivative of an ideal Euler product

Where the Dirichlet series indexed by the nonzero ideals converges absolutely, the L-series of the norm coefficients of a TauCeti.EulerProductData is the unrestricted product of its local Euler factors, by TauCeti.EulerProductData.hasProd_eulerFactor. A finite product has for logarithmic derivative the sum of the logarithmic derivatives of its factors. This file proves that the same holds for the infinite product: at every point strictly to the right of the ideal-indexed abscissa of absolute convergence at which no local factor vanishes, logDeriv of the L-series is the sum over the height-one primes of logDeriv of the local factors. Each summand is the negative quotient of a log-weighted prime-power series by its local factor, by TauCeti.EulerProductData.logDeriv_eulerFactor_eq.

Differentiating an infinite product is not a formal consequence of the pointwise product formula: it needs the convergence to be locally uniform, and that is what absolute convergence at a real point σ further left supplies. On the half-plane Re z > σ the deviation of the local factor at P from 1 is bounded, uniformly in z, by the prime-power tail ∑_{e ≥ 1} ‖D(P ^ e)‖ N(P) ^ (-e σ), and those tails are summable over the primes. That majorant is exactly what Summable.hasProdLocallyUniformlyOn_one_add asks for, so the partial Euler products converge to the L-series locally uniformly on the half-plane, and Complex.logDeriv_tendsto carries their logarithmic derivatives to that of the limit. The logarithmic derivative of a partial product is the corresponding finite sum, by logDeriv_fun_prod, so the limit is the asserted infinite sum.

The nonvanishing hypothesis is stated on the local factors, as for the logarithm itself in TauCeti/NumberTheory/ArithmeticDirichletSeries/EulerProduct/Logarithm/Data.lean; by TauCeti.EulerProductData.LSeries_eq_zero_iff_exists_eulerFactor_eq_zero it is equivalent to nonvanishing of the L-series, and for a completely multiplicative weight it is automatic.

Main results

• TauCeti.EulerProductData.hasSum_logDeriv_eulerFactor and TauCeti.EulerProductData.logDeriv_LSeries_eq_tsum_logDeriv_eulerFactor: the logarithmic derivative of the L-series is the sum of the local logarithmic derivatives.
• TauCeti.MultiplicativeIdealWeight.hasSum_logDeriv_eulerFactor and TauCeti.MultiplicativeIdealWeight.logDeriv_LSeries_eq_tsum_logDeriv_eulerFactor: the same for a completely multiplicative weight, where absolute convergence alone supplies the nonvanishing.

References

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

theorem TauCeti.EulerProductData.hasSum_logDeriv_eulerFactor {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) : HasSum (fun (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => logDeriv (D.eulerFactor P) s) (logDeriv (LSeries ⇑((normCoeff K) D.toIdealArithmeticFunction)) s)

The logarithmic derivative of an ideal Euler product is the sum of the local logarithmic derivatives. Strictly to the right of the ideal-indexed abscissa of absolute convergence, and at a point where no local Euler factor vanishes, the family of logarithmic derivatives of the local factors is summable over the height-one primes, with sum the logarithmic derivative of the L-series of the norm coefficients.

theorem TauCeti.EulerProductData.logDeriv_LSeries_eq_tsum_logDeriv_eulerFactor {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) : logDeriv (LSeries ⇑((normCoeff K) D.toIdealArithmeticFunction)) s = ∑' (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), logDeriv (D.eulerFactor P) s

The logarithmic derivative of an ideal Euler product, as a sum over the primes. The tsum form of TauCeti.EulerProductData.hasSum_logDeriv_eulerFactor.

theorem TauCeti.MultiplicativeIdealWeight.hasSum_logDeriv_eulerFactor {K : Type u_1} [Field K] [NumberField K] (χ : MultiplicativeIdealWeight K) {s : ℂ} (hs : idealAbscissaOfAbsConv K χ.toIdealArithmeticFunction < ↑s.re) : HasSum (fun (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => logDeriv ((EulerProductData.ofMultiplicativeIdealWeight χ).eulerFactor P) s) (logDeriv (LSeries ⇑((normCoeff K) χ.toIdealArithmeticFunction)) s)

The logarithmic derivative of the Euler product of a completely multiplicative weight. A degree-one weight has local factors (1 - χ(P) N(P) ^ (-s))⁻¹, which absolute convergence already keeps away from 0, so no nonvanishing hypothesis is needed here.

theorem TauCeti.MultiplicativeIdealWeight.logDeriv_LSeries_eq_tsum_logDeriv_eulerFactor {K : Type u_1} [Field K] [NumberField K] (χ : MultiplicativeIdealWeight K) {s : ℂ} (hs : idealAbscissaOfAbsConv K χ.toIdealArithmeticFunction < ↑s.re) : logDeriv (LSeries ⇑((normCoeff K) χ.toIdealArithmeticFunction)) s = ∑' (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), logDeriv ((EulerProductData.ofMultiplicativeIdealWeight χ).eulerFactor P) s

The logarithmic derivative of a completely multiplicative Euler product, as a sum over the primes. The tsum form of TauCeti.MultiplicativeIdealWeight.hasSum_logDeriv_eulerFactor.