Boundary data from the Dedekind zeta function

The Dedekind zeta function of a number field continues meromorphically across Re s = 1, has a simple pole at 1, and has no zeros on that line. Consequently its logarithmic derivative, after subtracting the pole, extends continuously to the closed half-plane. This file packages that analytic information as TauCeti.LFunctions.primeIdealVonMangoldtBoundary, the input expected by the generic prime-number-theorem transfer for the set of all prime ideals.

Main results

• TauCeti.LFunctions.primeIdealVonMangoldtBoundary: boundary data with residue one for all prime ideals of a number field.
• TauCeti.LFunctions.primeIdealVonMangoldtBoundary_series: its series is -ζ_K'/ζ_K on Re s > 1.

References

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

noncomputable def TauCeti.LFunctions.primeIdealVonMangoldtBoundary (K : Type u_1) [Field K] [NumberField K] : PrimeBoundaryRemainder K Set.univ 1

Boundary data for all primes of a number field. The von Mangoldt series of all primes of K sums to -ζ_K'(s)/ζ_K(s) on Re s > 1, and -ζ_K'(s)/ζ_K(s) - 1/(s - 1) extends continuously to Re s ≥ 1 (TauCeti.exists_continuousOn_eq_neg_deriv_dedekindZeta_div_sub).

Equations

• TauCeti.LFunctions.primeIdealVonMangoldtBoundary K = TauCeti.PrimeBoundaryRemainder.ofDedekindZeta ⋯.choose ⋯ ⋯

@[simp]

theorem TauCeti.LFunctions.primeIdealVonMangoldtBoundary_series {K : Type u_1} [Field K] [NumberField K] (s : { s : ℂ // 1 < s.re }) : (primeIdealVonMangoldtBoundary K).series s = -deriv (NumberField.dedekindZeta K) ↑s / NumberField.dedekindZeta K ↑s

The series of primeIdealVonMangoldtBoundary K is the negative logarithmic derivative -ζ_K'(s)/ζ_K(s) of the Dedekind zeta function on Re s > 1.