Formal logarithmic-derivative coefficients of an ideal Euler product

An EulerProductData K has at every height-one prime P a canonical local power series

F_P(X) = ∑ e, D(P ^ e) X ^ e.

Its formal logarithm log F_P packages the general prime-power logarithmic expansion, including coefficient systems whose values at higher prime powers are independent. The series

X * F_P'(X) / F_P(X)

then packages the local coefficients of the negative analytic logarithmic derivative: after substituting X = N(P) ^ (-s), its coefficient in degree e is multiplied by log N(P).

The identity (X F_P'/F_P) F_P = X F_P' gives a finite recurrence for every coefficient. In degrees one and two the coefficients are respectively D(P) and 2 D(P ^ 2) - D(P) ^ 2. For completely multiplicative degree-one data this reduces to the familiar geometric family χ(P) ^ e, so the general construction agrees with the existing prime-power logarithmic derivative rather than defining a parallel specialization.

These are formal identities: evaluating the logarithm series and differentiating it termwise are separate analytic questions requiring convergence hypotheses.

Main definitions

• TauCeti.EulerProductData.localLogSeries: the formal logarithm of a local Euler factor.
• TauCeti.EulerProductData.localLogDerivSeries: the series X F_P'/F_P.

Main results

• TauCeti.EulerProductData.sum_antidiagonal_coeff_localLogDerivSeries_eq: the coefficient recurrence determining the local logarithmic derivative.
• TauCeti.EulerProductData.coeff_localLogDerivSeries_ofMultiplicativeIdealWeight: the specialization to completely multiplicative weights.

References

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

noncomputable def TauCeti.EulerProductData.localLogSeries {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : PowerSeries ℂ

The formal logarithm of the local power series of D at P. Its constant coefficient is zero because coprime multiplicativity fixes the constant coefficient of the local series to be one.

Equations

• D.localLogSeries P = (D.localPowerSeries P).logOf

theorem TauCeti.EulerProductData.localLogSeries_def {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : D.localLogSeries P = (D.localPowerSeries P).logOf

The local logarithm is the formal logarithm of the local power series.

noncomputable def TauCeti.EulerProductData.localLogDerivSeries {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : PowerSeries ℂ

The local formal logarithmic-derivative series X F_P'(X) / F_P(X). The factor X aligns degree e with the prime power P ^ e; after substituting X = N(P) ^ (-s), these are the coefficients of the negative analytic logarithmic derivative before multiplication by log N(P).

Equations

• D.localLogDerivSeries P = PowerSeries.X * (D.localPowerSeries P).logDeriv

theorem TauCeti.EulerProductData.localLogDerivSeries_def {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : D.localLogDerivSeries P = PowerSeries.X * (D.localPowerSeries P).logDeriv

The local logarithmic-derivative series is X times the formal logarithmic derivative of the local power series.

@[simp]

theorem TauCeti.EulerProductData.constantCoeff_localLogSeries {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : PowerSeries.constantCoeff (D.localLogSeries P) = 0

The formal local logarithm has zero constant coefficient.

@[simp]

theorem TauCeti.EulerProductData.coeff_zero_localLogDerivSeries {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : (PowerSeries.coeff 0) (D.localLogDerivSeries P) = 0

The degree-zero logarithmic-derivative coefficient vanishes.

theorem TauCeti.EulerProductData.coeff_succ_localLogDerivSeries {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (n : ℕ) : (PowerSeries.coeff (n + 1)) (D.localLogDerivSeries P) = (↑n + 1) * (PowerSeries.coeff (n + 1)) (D.localLogSeries P)

The coefficient in positive degree of X (log F_P)' is the degree times the corresponding coefficient of log F_P.

theorem TauCeti.EulerProductData.localLogDerivSeries_mul_localPowerSeries {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : D.localLogDerivSeries P * D.localPowerSeries P = PowerSeries.X * PowerSeries.derivative (D.localPowerSeries P)

The local logarithmic derivative is characterized by (X F_P'/F_P) * F_P = X F_P'.

theorem TauCeti.EulerProductData.sum_antidiagonal_coeff_localLogDerivSeries_eq {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (n : ℕ) : ∑ ij ∈ Finset.antidiagonal n, (PowerSeries.coeff ij.1) (D.localLogDerivSeries P) * D.toIdealArithmeticFunction (P.primeIdealPow ij.2) = ↑n * D.toIdealArithmeticFunction (P.primeIdealPow n)

The local logarithmic-derivative recurrence. If b e is the coefficient of X F_P'/F_P in degree e, then

sum_(i+j=n) b i * D(P ^ j) = n * D(P ^ n).

Because b 0 = 0 and D(P ^ 0) = 1, this determines b n from the preceding coefficients and the prime-power data through degree n.

@[simp]

theorem TauCeti.EulerProductData.coeff_one_localLogDerivSeries {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : (PowerSeries.coeff 1) (D.localLogDerivSeries P) = D.toIdealArithmeticFunction (P.primeIdealPow 1)

The first local logarithmic-derivative coefficient is the coefficient at P.

@[simp]

theorem TauCeti.EulerProductData.coeff_two_localLogDerivSeries {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : (PowerSeries.coeff 2) (D.localLogDerivSeries P) = 2 * D.toIdealArithmeticFunction (P.primeIdealPow 2) - D.toIdealArithmeticFunction (P.primeIdealPow 1) ^ 2

The second local logarithmic-derivative coefficient records the first genuinely independent prime-power datum: it is 2 D(P ^ 2) - D(P) ^ 2.

theorem TauCeti.EulerProductData.localPowerSeries_ofMultiplicativeIdealWeight {K : Type u_1} [Field K] [NumberField K] (χ : MultiplicativeIdealWeight K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : (ofMultiplicativeIdealWeight χ).localPowerSeries P = PowerSeries.mk fun (n : ℕ) => χ P.asIdeal ^ n

The local power series of completely multiplicative data is the geometric series with degree-n coefficient χ(P) ^ n.

theorem TauCeti.EulerProductData.localLogDerivSeries_ofMultiplicativeIdealWeight {K : Type u_1} [Field K] [NumberField K] (χ : MultiplicativeIdealWeight K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : (ofMultiplicativeIdealWeight χ).localLogDerivSeries P = PowerSeries.X * PowerSeries.C (χ P.asIdeal) * (ofMultiplicativeIdealWeight χ).localPowerSeries P

For completely multiplicative data, the local formal logarithmic derivative is the geometric family X * χ(P) * F_P(X).

@[simp]

theorem TauCeti.EulerProductData.coeff_localLogDerivSeries_ofMultiplicativeIdealWeight {K : Type u_1} [Field K] [NumberField K] (χ : MultiplicativeIdealWeight K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (n : ℕ) : (PowerSeries.coeff n) ((ofMultiplicativeIdealWeight χ).localLogDerivSeries P) = if n = 0 then 0 else χ P.asIdeal ^ n

The degree-n local logarithmic-derivative coefficient of a completely multiplicative weight is χ(P) ^ n for n > 0, and zero in degree zero.