Convergence of logarithmic-derivative series

The formal logarithmic derivative of a local Euler factor converges as far as the local power series is zero-free. This removes the independent coefficient-summability hypothesis from the evaluation theorem when zero-freeness is known on a disk. Combining the local result over all height-one primes gives the prime-power expansion of the global logarithmic derivative.

For a height-one prime P, absolute convergence at a real parameter σ gives convergence of the local power series on the disk of radius N(P)⁻σ. If that disk contains no zero, the formal logarithmic derivative converges at N(P) ^ (-s) for every s with σ < Re(s).

Main results

• TauCeti.EulerProductData.summable_norm_coeff_localLogDerivSeries_of_zeroFree: absolute convergence of the formal local logarithmic derivative in a zero-free disk.
• logDeriv_eulerFactor_eq_neg_log_mul_tsum_coeff_localLogDerivSeries_of_zeroFree: evaluation of the formal series without a separate summability hypothesis.
• TauCeti.EulerProductData.hasSum_tsum_coeff_localLogDerivSeries_of_zeroFree: the global prime-power expansion under uniform local zero-free disks.
• TauCeti.EulerProductData.exists_logarithm_hasSum_localLogDerivSeries: a holomorphic logarithm whose derivative is given by the global prime-power expansion.

References

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

theorem TauCeti.EulerProductData.summable_norm_coeff_localLogDerivSeries_of_zeroFree {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) {σ : ℝ} {s : ℂ} (hσ : LSeries.abscissaOfAbsConv ⇑(D.localArithmeticFactor P) < ↑σ) (hne : ∀ (z : ℂ), ‖z‖ < ‖↑(Ideal.absNorm P.asIdeal) ^ (-↑σ)‖ → FormalMultilinearSeries.ofScalarsSum (fun (n : ℕ) => (PowerSeries.coeff n) (D.localPowerSeries P)) z ≠ 0) (hs : σ < s.re) : Summable fun (e : ℕ) => ‖(PowerSeries.coeff e) (D.localLogDerivSeries P) * (↑(Ideal.absNorm P.asIdeal) ^ (-s)) ^ e‖

Absolute convergence of a local formal logarithmic derivative on a zero-free disk. Suppose the local factor at P converges absolutely at the real point σ, and its power series has no zero in the disk of radius ‖N(P) ^ (-σ)‖. Then its formal logarithmic derivative converges absolutely at N(P) ^ (-s) whenever σ < Re(s).

theorem TauCeti.EulerProductData.summable_coeff_localLogDerivSeries_of_zeroFree {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) {σ : ℝ} {s : ℂ} (hσ : LSeries.abscissaOfAbsConv ⇑(D.localArithmeticFactor P) < ↑σ) (hne : ∀ (z : ℂ), ‖z‖ < ‖↑(Ideal.absNorm P.asIdeal) ^ (-↑σ)‖ → FormalMultilinearSeries.ofScalarsSum (fun (n : ℕ) => (PowerSeries.coeff n) (D.localPowerSeries P)) z ≠ 0) (hs : σ < s.re) : Summable fun (e : ℕ) => (PowerSeries.coeff e) (D.localLogDerivSeries P) * (↑(Ideal.absNorm P.asIdeal) ^ (-s)) ^ e

Convergence of a local formal logarithmic derivative on a zero-free disk. Suppose the local factor at P converges absolutely at the real point σ, and its power series has no zero in the disk of radius ‖N(P) ^ (-σ)‖. Then its formal logarithmic derivative converges at N(P) ^ (-s) whenever σ < Re(s).

theorem TauCeti.EulerProductData.eulerFactor_ne_zero_of_zeroFree {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) {σ : ℝ} {s : ℂ} (hne : ∀ (z : ℂ), ‖z‖ < ‖↑(Ideal.absNorm P.asIdeal) ^ (-↑σ)‖ → FormalMultilinearSeries.ofScalarsSum (fun (n : ℕ) => (PowerSeries.coeff n) (D.localPowerSeries P)) z ≠ 0) (hs : σ < s.re) : D.eulerFactor P s ≠ 0

A local Euler factor is nonzero at s if the corresponding local power series is zero-free on the disk bounded by the real parameter σ, and σ < Re(s).

theorem TauCeti.EulerProductData.logDeriv_eulerFactor_eq_neg_log_mul_tsum_coeff_localLogDerivSeries_of_zeroFree {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) {σ : ℝ} {s : ℂ} (hσ : LSeries.abscissaOfAbsConv ⇑(D.localArithmeticFactor P) < ↑σ) (hne : ∀ (z : ℂ), ‖z‖ < ‖↑(Ideal.absNorm P.asIdeal) ^ (-↑σ)‖ → FormalMultilinearSeries.ofScalarsSum (fun (n : ℕ) => (PowerSeries.coeff n) (D.localPowerSeries P)) z ≠ 0) (hs : σ < s.re) : logDeriv (D.eulerFactor P) s = -Complex.log ↑(Ideal.absNorm P.asIdeal) * ∑' (e : ℕ), (PowerSeries.coeff e) (D.localLogDerivSeries P) * (↑(Ideal.absNorm P.asIdeal) ^ (-s)) ^ e

The evaluation of a local formal logarithmic derivative inside a zero-free disk. This is logDeriv_eulerFactor_eq_neg_log_mul_tsum_coeff_localLogDerivSeries with coefficient convergence deduced from zero-freeness.

theorem TauCeti.EulerProductData.hasSum_tsum_coeff_localLogDerivSeries_of_zeroFree {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) {σ : ℝ} {s : ℂ} (hσ : idealAbscissaOfAbsConv K D.toIdealArithmeticFunction < ↑σ) (hne : ∀ (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (z : ℂ), ‖z‖ < ‖↑(Ideal.absNorm P.asIdeal) ^ (-↑σ)‖ → FormalMultilinearSeries.ofScalarsSum (fun (n : ℕ) => (PowerSeries.coeff n) (D.localPowerSeries P)) z ≠ 0) (hs : σ < s.re) : 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 global logarithmic derivative expanded over prime powers. Suppose σ lies strictly to the right of the ideal-indexed abscissa of absolute convergence and every local power series is zero-free on the disk of radius N(P)⁻σ. For Re(s) > σ, the local formal logarithmic derivatives then converge, and their prime-indexed sum is the logarithmic derivative of the global L-series.

theorem TauCeti.EulerProductData.logDeriv_LSeries_eq_tsum_tsum_coeff_localLogDerivSeries_of_zeroFree {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) {σ : ℝ} {s : ℂ} (hσ : idealAbscissaOfAbsConv K D.toIdealArithmeticFunction < ↑σ) (hne : ∀ (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (z : ℂ), ‖z‖ < ‖↑(Ideal.absNorm P.asIdeal) ^ (-↑σ)‖ → FormalMultilinearSeries.ofScalarsSum (fun (n : ℕ) => (PowerSeries.coeff n) (D.localPowerSeries P)) z ≠ 0) (hs : σ < s.re) : 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_of_zeroFree.

theorem TauCeti.EulerProductData.exists_logarithm_hasSum_localLogDerivSeries {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) {U : Set ℂ} {σ : ℝ} (hUc : IsSimplyConnected U) (hUo : IsOpen U) (hσ : idealAbscissaOfAbsConv K D.toIdealArithmeticFunction < ↑σ) (hU : ∀ s ∈ U, σ < s.re) (hne : ∀ (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (z : ℂ), ‖z‖ < ‖↑(Ideal.absNorm P.asIdeal) ^ (-↑σ)‖ → FormalMultilinearSeries.ofScalarsSum (fun (n : ℕ) => (PowerSeries.coeff n) (D.localPowerSeries P)) z ≠ 0) : ∃ (L : ℂ → ℂ), DifferentiableOn ℂ L U ∧ Set.EqOn (Complex.exp ∘ L) (LSeries ⇑((normCoeff K) D.toIdealArithmeticFunction)) U ∧ ∀ s ∈ U, 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) (deriv L s)

A holomorphic logarithm with its derivative expanded over prime powers. On a simply connected open set contained in Re(s) > σ, the L-series has a holomorphic logarithm, and the derivative of that branch is the global sum of the local formal logarithmic-derivative series. The local zero-free disk hypothesis is what makes each formal series converge throughout the region.