The von Mangoldt series of all prime ideals is `-ζ_K'/ζ_K` #

Over all height-one primes of a number field K, the coefficient system TauCeti.primeVonMangoldtCoeff K Set.univ is the norm regrouping of the ideal von Mangoldt function Λ_K, whose partial sums are Chebyshev's ψ_K. This file identifies its Dirichlet series on Re s > 1 with the negative logarithmic derivative of the Dedekind zeta function:

∑ n, primeVonMangoldtCoeff K Set.univ n · n^{-s} = ∑_A Λ_K(A) N(A)^{-s} = -ζ_K'(s) / ζ_K(s)

This is the number-field analogue of Mathlib's ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div. It is the trivial-weight case of TauCeti.MultiplicativeIdealWeight.logDeriv_LSeries_eq_neg_tsum_vonMangoldtTransform, since the trivial weight regroups to ζ_K (TauCeti.dedekindZeta_eq_LSeries_normCoeff_one) and its von Mangoldt transform is Λ_K.

The constructor TauCeti.PrimeBoundaryRemainder.ofDedekindZeta obtains the series condition of the boundary data TauCeti.PrimeBoundaryRemainder K Set.univ 1 from this identity, and builds the package from a single function G, continuous on Re s ≥ 1, that agrees with -ζ_K'(s)/ζ_K(s) - 1/(s - 1) on Re s > 1. The unconditional construction of such a function belongs to the analytic theory of the Dedekind zeta function.

Main results #

TauCeti.hasSum_idealTerm_vonMangoldt: the ideal-indexed series of Λ_K sums to -ζ_K'(s)/ζ_K(s) on Re s > 1.
TauCeti.LSeriesHasSum_primeVonMangoldtCoeff_univ and TauCeti.LSeries_primeVonMangoldtCoeff_univ_eq_deriv_dedekindZeta_div: the same for the norm-regrouped coefficients, in Mathlib's LSeries vocabulary.
TauCeti.PrimeBoundaryRemainder.ofDedekindZeta: boundary data with residue one for all primes from a continuous extension of -ζ_K'/ζ_K - 1/(s - 1) to Re s ≥ 1.

References #

J. Neukirch, Algebraic Number Theory, Chapter VII, §5.
H. Davenport, Multiplicative Number Theory, Chapter 17.

source

theorem TauCeti.hasSum_idealTerm_vonMangoldt {K : Type u_1} [Field K] [NumberField K] {s : ℂ} (hs : 1 < s.re) :

HasSum (idealTerm K IdealArithmeticFunction.vonMangoldt s) (-deriv (NumberField.dedekindZeta K) s / NumberField.dedekindZeta K s)

The von Mangoldt series of K is -ζ_K'/ζ_K. On Re s > 1 the ideal-indexed series ∑_A Λ_K(A) N(A)^{-s} converges absolutely to -ζ_K'(s) / ζ_K(s).

source

theorem TauCeti.LSeriesHasSum_primeVonMangoldtCoeff_univ {K : Type u_1} [Field K] [NumberField K] {s : ℂ} (hs : 1 < s.re) :

LSeriesHasSum (fun (n : ℕ) => ↑((primeVonMangoldtCoeff K Set.univ) n)) s (-deriv (NumberField.dedekindZeta K) s / NumberField.dedekindZeta K s)

The von Mangoldt coefficients of all primes have Dirichlet series -ζ_K'/ζ_K. On Re s > 1 the series of TauCeti.primeVonMangoldtCoeff K Set.univ converges absolutely to -ζ_K'(s) / ζ_K(s). This is the LSeriesHasSum field of TauCeti.PrimeBoundaryRemainder K Set.univ δ, with an explicit sum.

source

theorem TauCeti.LSeries_primeVonMangoldtCoeff_univ_eq_deriv_dedekindZeta_div {K : Type u_1} [Field K] [NumberField K] {s : ℂ} (hs : 1 < s.re) :

LSeries (fun (n : ℕ) => ↑((primeVonMangoldtCoeff K Set.univ) n)) s = -deriv (NumberField.dedekindZeta K) s / NumberField.dedekindZeta K s

On Re s > 1 the LSeries of the von Mangoldt coefficients of all primes is -ζ_K'(s) / ζ_K(s).

source

noncomputable def TauCeti.PrimeBoundaryRemainder.ofDedekindZeta {K : Type u_1} [Field K] [NumberField K] (G : ℂ → ℂ) (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (hGζ : ∀ (s : ℂ), 1 < s.re → G s = -deriv (NumberField.dedekindZeta K) s / NumberField.dedekindZeta K s - 1 / (s - 1)) :

PrimeBoundaryRemainder K Set.univ 1

Boundary data for all primes from the Dedekind zeta function. A function G, continuous on Re s ≥ 1, that agrees on Re s > 1 with -ζ_K'(s)/ζ_K(s) - 1/(s - 1) is the whole of the analytic input to TauCeti.PrimeBoundaryRemainder K Set.univ 1: the series is -ζ_K'/ζ_K by TauCeti.LSeriesHasSum_primeVonMangoldtCoeff_univ.

Equations