Derivatives of ideal Euler factors and logarithmic expansions

For general TauCeti.EulerProductData, this file first differentiates each local Euler factor. The derivative at a prime P is the exact prime-power series

-∑ e, log N(P ^ e) · D(P ^ e) / N(P ^ e) ^ s.

This is the local analytic input for expressing the logarithmic derivative of a general ideal Euler product in terms of its prime-power data. The second part of the file specializes to a completely multiplicative weight, where the logarithm itself has a geometric Taylor expansion and can be differentiated after summing over all primes and exponents.

TauCeti.MultiplicativeIdealWeight.tsum_prime_pow_eq_tsum_neg_log_one_sub expands the sum of local logarithms over the prime powers (P, e). This file differentiates that expansion in s, term by term, on the open half-plane where the ideal-indexed series converges absolutely.

Each term (χ(P) N(P)⁻ˢ) ^ (e+1) / (e+1) differentiates to -log N(P) * (χ(P) N(P)⁻ˢ) ^ (e+1), so the differentiated family is the undivided one weighted by -log N(P). Termwise differentiation of a sum needs a summable majorant valid across a neighbourhood rather than at the single point, and the half-plane supplies it: strictly to the right of a point of absolute convergence the weight log N(P) is absorbed, which is summable_log_absNorm_mul_norm_idealTerm_of_re_lt_re, and the exponent direction is geometric, which is TauCeti.summable_mul_norm_pow_succ.

EulerProduct/Branch.lean identifies the derivative of a branch of the logarithm with the logarithmic derivative of the L-series. That is an abstract identification; this file gives the prime-power series the derivative is equal to.

Main results

• TauCeti.EulerProductData.hasDerivAt_eulerFactor: a general local Euler factor differentiates termwise into the negative of its log-weighted prime-power series.
• TauCeti.EulerProductData.logDeriv_eulerFactor_eq: the local factor's logarithmic derivative is the negative quotient of that prime-power series by the local factor.
• TauCeti.MultiplicativeIdealWeight.hasDerivAt_tsum_prime_pow: the prime-power expansion differentiates termwise, strictly right of the abscissa of absolute convergence.
• TauCeti.MultiplicativeIdealWeight.logDeriv_LSeries_eq_tsum_prime_pow: that derivative is the logarithmic derivative of the L-series.

Derivative of a general local Euler factor

theorem TauCeti.EulerProductData.LSeries_logMul_localArithmeticFactor_eq_tsum {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (s : ℂ) : LSeries (LSeries.logMul ⇑(D.localArithmeticFactor P)) s = ∑' (e : ℕ), Complex.log ↑(Ideal.absNorm ↑(P.primeIdealPow e)) * idealTerm K D.toIdealArithmeticFunction s (P.primeIdealPow e)

The L-series of the logarithmically weighted local arithmetic factor is the corresponding prime-power series. This is an unconditional identity of totalized sums; its useful applications are on the half-plane where the local series converges.

theorem TauCeti.EulerProductData.summable_log_absNorm_mul_idealTerm_primeIdealPow {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) : Summable fun (e : ℕ) => Complex.log ↑(Ideal.absNorm ↑(P.primeIdealPow e)) * idealTerm K D.toIdealArithmeticFunction s (P.primeIdealPow e)

The log-weighted prime-power series for a local Euler factor is summable on its half-plane of absolute convergence.

theorem TauCeti.EulerProductData.hasDerivAt_eulerFactor {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) : HasDerivAt (D.eulerFactor P) (-∑' (e : ℕ), Complex.log ↑(Ideal.absNorm ↑(P.primeIdealPow e)) * idealTerm K D.toIdealArithmeticFunction s (P.primeIdealPow e)) s

A general local Euler factor differentiates termwise. Strictly to the right of its abscissa of absolute convergence, the derivative of the factor at P is the negative of the log-weighted series over the powers of P.

theorem TauCeti.EulerProductData.deriv_eulerFactor {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) : deriv (D.eulerFactor P) s = -∑' (e : ℕ), Complex.log ↑(Ideal.absNorm ↑(P.primeIdealPow e)) * idealTerm K D.toIdealArithmeticFunction s (P.primeIdealPow e)

The derivative of a general local Euler factor is the negative of its log-weighted prime-power series.

theorem TauCeti.EulerProductData.logDeriv_eulerFactor_eq {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) : logDeriv (D.eulerFactor P) s = (-∑' (e : ℕ), Complex.log ↑(Ideal.absNorm ↑(P.primeIdealPow e)) * idealTerm K D.toIdealArithmeticFunction s (P.primeIdealPow e)) / D.eulerFactor P s

The logarithmic derivative of a local factor is the negative quotient of its log-weighted prime-power series by the factor itself.

theorem TauCeti.MultiplicativeIdealWeight.hasDerivAt_prime_pow_taylor_term {K : Type u_1} [Field K] [NumberField K] (χ : MultiplicativeIdealWeight K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (e : ℕ) (s : ℂ) : HasDerivAt (fun (z : ℂ) => (χ P.asIdeal / ↑(Ideal.absNorm P.asIdeal) ^ z) ^ (e + 1) / (↑e + 1)) (-(Complex.log ↑(Ideal.absNorm P.asIdeal) * (χ P.asIdeal / ↑(Ideal.absNorm P.asIdeal) ^ s) ^ (e + 1))) s

The Taylor term at (P, e) differentiates to -log N(P) times the undivided power. The division by e + 1 is what makes the derivative the plain power rather than a multiple of it.

theorem TauCeti.MultiplicativeIdealWeight.norm_log_mul_prime_pow_le {K : Type u_1} [Field K] [NumberField K] (χ : MultiplicativeIdealWeight K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (e : ℕ) {σ₀ : ℝ} {z : ℂ} (hz : σ₀ ≤ z.re) : ‖-(Complex.log ↑(Ideal.absNorm P.asIdeal) * (χ P.asIdeal / ↑(Ideal.absNorm P.asIdeal) ^ z) ^ (e + 1))‖ ≤ Real.log ↑(Ideal.absNorm P.asIdeal) * ‖χ P.asIdeal / ↑(Ideal.absNorm P.asIdeal) ^ ↑σ₀‖ ^ (e + 1)

The differentiated term is dominated by its value at the edge of the half-plane. The bound is uniform in z across σ₀ ≤ z.re, which is what termwise differentiation of a sum requires.

theorem TauCeti.MultiplicativeIdealWeight.summable_log_absNorm_mul_norm_prime_pow {K : Type u_1} [Field K] [NumberField K] (χ : MultiplicativeIdealWeight K) {s s' : ℂ} (h : s.re < s'.re) (hs : Summable (idealTerm K χ.toIdealArithmeticFunction s)) : Summable fun (pe : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K) × ℕ) => Real.log ↑(Ideal.absNorm pe.1.asIdeal) * ‖χ pe.1.asIdeal / ↑(Ideal.absNorm pe.1.asIdeal) ^ s'‖ ^ (pe.2 + 1)

The log-weighted majorant is summable over primes and exponents together. Strictly to the right of a point of absolute convergence the weight log N(P) is absorbed, and the exponent direction is geometric.

theorem TauCeti.MultiplicativeIdealWeight.hasDerivAt_tsum_prime_pow {K : Type u_1} [Field K] [NumberField K] (χ : MultiplicativeIdealWeight K) {s : ℂ} (hs : idealAbscissaOfAbsConv K χ.toIdealArithmeticFunction < ↑s.re) : HasDerivAt (fun (z : ℂ) => ∑' (pe : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K) × ℕ), (χ pe.1.asIdeal / ↑(Ideal.absNorm pe.1.asIdeal) ^ z) ^ (pe.2 + 1) / (↑pe.2 + 1)) (∑' (pe : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K) × ℕ), -(Complex.log ↑(Ideal.absNorm pe.1.asIdeal) * (χ pe.1.asIdeal / ↑(Ideal.absNorm pe.1.asIdeal) ^ s) ^ (pe.2 + 1))) s

The prime-power expansion differentiates termwise. Strictly to the right of the abscissa of absolute convergence, the sum over prime powers is differentiable and its derivative is the termwise one: the same family weighted by -log N(P), with the division by e + 1 gone.

The abscissa is all that is needed: convergence propagates rightward from any point to its left, which is what supplies the majorant on a neighbourhood of s.

theorem TauCeti.MultiplicativeIdealWeight.logDeriv_LSeries_eq_tsum_prime_pow {K : Type u_1} [Field K] [NumberField K] (χ : MultiplicativeIdealWeight K) {s : ℂ} (hs : idealAbscissaOfAbsConv K χ.toIdealArithmeticFunction < ↑s.re) : logDeriv (LSeries ⇑((normCoeff K) χ.toIdealArithmeticFunction)) s = ∑' (pe : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K) × ℕ), -(Complex.log ↑(Ideal.absNorm pe.1.asIdeal) * (χ pe.1.asIdeal / ↑(Ideal.absNorm pe.1.asIdeal) ^ s) ^ (pe.2 + 1))

The logarithmic derivative of the L-series, as a prime-power series. Strictly to the right of a point of absolute convergence,

logDeriv L(s) = ∑' (P, e), -log N(P) · (χ(P) N(P)⁻ˢ) ^ (e+1)

strictly to the right of the abscissa of absolute convergence.

The prime-power expansion is a branch of the logarithm of the L-series there — its exponential is the L-series, by exp_tsum_prime_pow_eq_LSeries — and the derivative of any such branch is the logarithmic derivative, the branch ambiguity being locally constant.

This is what lets a density argument work with the logarithmic derivative termwise over prime powers, rather than with the L-series itself.