Boundary data for prime-counting Dirichlet series

For a set S of prime ideals of a number field, the logarithmically weighted prime-power coefficients TauCeti.primeVonMangoldtCoeff K S are nonnegative and have partial sums equal to Chebyshev's function TauCeti.primePsi K S. This file packages the exact analytic boundary data that lets the Wiener--Ikehara theorem act on those coefficients.

TauCeti.PrimeBoundaryRemainder K S δ consists of the sum of their Dirichlet series on Re s > 1, together with a continuous extension to Re s ≥ 1 of the remainder after subtracting the pole δ / (s - 1). The two functions are defined on these half-plane subtypes rather than on all of ℂ; values outside the regions used by the hypotheses are therefore not carried as free data. PrimeBoundaryRemainder.ofFunctions constructs the package from the whole-plane functions that naturally occur in analytic applications.

The main theorem TauCeti.primeNumberTheoremTransfer combines Wiener--Ikehara, removal of higher prime powers, and Abel summation. It gives the error-term forms of all three conclusions ψ(x) = δx + o(x), ϑ(x) = δx + o(x), and π(x) = δ Li(x) + o(x / log x), including δ = 0. The conditional specialization TauCeti.primeIdealTheorem_of_boundary records the usual prime ideal theorem once boundary data with residue one is available.

Main results

• TauCeti.PrimeBoundaryRemainder: boundary data with residue δ for the prime Dirichlet series of S, with the constructor TauCeti.PrimeBoundaryRemainder.ofFunctions.
• TauCeti.primeNumberTheoremTransfer: boundary data give the asymptotics of ψ, ϑ, and π.
• TauCeti.primeIdealTheorem_of_boundary: the prime ideal theorem from boundary data with residue one.
• TauCeti.primeCount_sub_mul_logIntegral_isLittleO_of_LSeriesSummable_sub: comparison with a Dirichlet series L(c, s). If L(c, s) - δ / (s - 1) extends continuously to Re s ≥ 1 and the Dirichlet series of the coefficient difference converges absolutely at s = 1, then π_S(x) = δ Li(x) + o(x / log x).

References

• H. Davenport, Multiplicative Number Theory, Chapters 1 and 17.
• J. Korevaar, Tauberian Theory: A Century of Developments, Chapter III.
• G. Tenenbaum, Introduction to Analytic and Probabilistic Number Theory, Chapter II.

structure TauCeti.PrimeBoundaryRemainder (K : Type u_2) [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (δ : ℝ) : Type

Boundary data for the prime Dirichlet series of S. The function series is the sum of the Dirichlet series of primeVonMangoldtCoeff K S on Re s > 1. The function remainder is continuous on Re s ≥ 1 and agrees on the open half-plane with series s - δ / (s - 1).

The functions have precisely their mathematically relevant domains, so the structure carries no arbitrary values elsewhere.

• series : { s : ℂ // 1 < s.re } → ℂ

  The sum of the von Mangoldt Dirichlet series on Re s > 1.

• remainder : { s : ℂ // 1 ≤ s.re } → ℂ

  The continuous pole-subtracted remainder on Re s ≥ 1.

• hasSum (s : { s : ℂ // 1 < s.re }) : LSeriesHasSum (fun (n : ℕ) => ↑((primeVonMangoldtCoeff K S) n)) (↑s) (self.series s)

  The named function series is the sum of the exact von Mangoldt coefficient series.

• continuous_remainder : Continuous self.remainder

  The pole-subtracted remainder is continuous on the closed half-plane.

• remainder_eq (s : { s : ℂ // 1 < s.re }) : self.remainder ⟨↑s, ⋯⟩ = self.series s - ↑δ / (↑s - 1)

  On Re s > 1, the remainder is the series with its pole subtracted.

theorem TauCeti.PrimeBoundaryRemainder.ext {K : Type u_2} {inst✝ : Field K} {inst✝¹ : NumberField K} {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {δ : ℝ} {x y : PrimeBoundaryRemainder K S δ} (series : x.series = y.series) (remainder : x.remainder = y.remainder) : x = y

theorem TauCeti.PrimeBoundaryRemainder.ext_iff {K : Type u_2} {inst✝ : Field K} {inst✝¹ : NumberField K} {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {δ : ℝ} {x y : PrimeBoundaryRemainder K S δ} : x = y ↔ x.series = y.series ∧ x.remainder = y.remainder

def TauCeti.PrimeBoundaryRemainder.ofFunctions {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {δ : ℝ} (F G : ℂ → ℂ) (hF : ∀ (s : ℂ), 1 < s.re → LSeriesHasSum (fun (n : ℕ) => ↑((primeVonMangoldtCoeff K S) n)) s (F s)) (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (hGF : ∀ (s : ℂ), 1 < s.re → G s = F s - ↑δ / (s - 1)) : PrimeBoundaryRemainder K S δ

Construct prime boundary data from functions on the whole complex plane. Only their restrictions to Re s > 1 and Re s ≥ 1 are retained.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.PrimeBoundaryRemainder.ofFunctions_series {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {δ : ℝ} (F G : ℂ → ℂ) (hF : ∀ (s : ℂ), 1 < s.re → LSeriesHasSum (fun (n : ℕ) => ↑((primeVonMangoldtCoeff K S) n)) s (F s)) (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (hGF : ∀ (s : ℂ), 1 < s.re → G s = F s - ↑δ / (s - 1)) (s : { s : ℂ // 1 < s.re }) : (ofFunctions F G hF hG hGF).series s = F ↑s

@[simp]

theorem TauCeti.PrimeBoundaryRemainder.ofFunctions_remainder {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {δ : ℝ} (F G : ℂ → ℂ) (hF : ∀ (s : ℂ), 1 < s.re → LSeriesHasSum (fun (n : ℕ) => ↑((primeVonMangoldtCoeff K S) n)) s (F s)) (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (hGF : ∀ (s : ℂ), 1 < s.re → G s = F s - ↑δ / (s - 1)) (s : { s : ℂ // 1 ≤ s.re }) : (ofFunctions F G hF hG hGF).remainder s = G ↑s

theorem TauCeti.PrimeBoundaryRemainder.tendsto_inv_mul_primePsi {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {δ : ℝ} (B : PrimeBoundaryRemainder K S δ) : Filter.Tendsto (fun (x : ℝ) => x⁻¹ * primePsi K S x) Filter.atTop (nhds δ)

Wiener--Ikehara applied to a prime boundary package: the normalized ψ function tends to the residue δ.

theorem TauCeti.PrimeBoundaryRemainder.nonneg {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {δ : ℝ} (B : PrimeBoundaryRemainder K S δ) : 0 ≤ δ

Boundary data force the residue to be nonnegative; it need not be carried as a redundant field because ψ(x) / x is eventually nonnegative and tends to δ.

theorem TauCeti.primePsi_asymptotic_of_boundary {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {δ : ℝ} (B : PrimeBoundaryRemainder K S δ) : (fun (x : ℝ) => primePsi K S x - δ * x) =o[Filter.atTop] fun (x : ℝ) => x

The Tauberian asymptotic for Chebyshev's ψ. Exact prime boundary data with residue δ imply ψ(x) = δx + o(x).

theorem TauCeti.primeNumberTheoremTransfer {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {δ : ℝ} (B : PrimeBoundaryRemainder K S δ) : ((fun (x : ℝ) => primePsi K S x - δ * x) =o[Filter.atTop] fun (x : ℝ) => x) ∧ ((fun (x : ℝ) => primeTheta K S x - δ * x) =o[Filter.atTop] fun (x : ℝ) => x) ∧ (fun (x : ℝ) => primeCount K S x - δ * Real.logIntegral x) =o[Filter.atTop] fun (x : ℝ) => x / Real.log x

Prime-number-theorem transfer from exact boundary data. The three conclusions are, respectively, the von Mangoldt-weighted prime-power asymptotic, the logarithmically weighted prime asymptotic after removing higher powers, and the unweighted prime-counting asymptotic after Abel summation. The error-term formulation includes residue zero.

theorem TauCeti.primeCount_sub_mul_logIntegral_isLittleO_of_LSeriesSummable_sub {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {δ : ℝ} {c : ℕ → ℂ} {G : ℂ → ℂ} (hc : LSeries.abscissaOfAbsConv c ≤ 1) (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (hGc : Set.EqOn G (fun (s : ℂ) => LSeries c s - ↑δ / (s - 1)) {s : ℂ | 1 < s.re}) (hd : LSeriesSummable (fun (n : ℕ) => ↑((primeVonMangoldtCoeff K S) n) - c n) 1) : (fun (x : ℝ) => primeCount K S x - δ * Real.logIntegral x) =o[Filter.atTop] fun (x : ℝ) => x / Real.log x

Prime counting by comparison with a Dirichlet series. Let c be coefficients whose Dirichlet series converges absolutely on Re s > 1 and such that L(c, s) - δ / (s - 1) agrees there with a function G continuous on Re s ≥ 1. If the Dirichlet series of the difference between primeVonMangoldtCoeff K S and c converges absolutely at s = 1, then π_S(x) = δ Li(x) + o(x / log x).

theorem TauCeti.primeIdealTheorem_of_boundary {K : Type u_1} [Field K] [NumberField K] (B : PrimeBoundaryRemainder K Set.univ 1) : (Asymptotics.IsEquivalent Filter.atTop (primePsi K Set.univ) fun (x : ℝ) => x) ∧ (Asymptotics.IsEquivalent Filter.atTop (primeTheta K Set.univ) fun (x : ℝ) => x) ∧ Asymptotics.IsEquivalent Filter.atTop (primeCount K Set.univ) Real.logIntegral

The conditional prime ideal theorem. Boundary data for all prime ideals with residue one give the standard asymptotic equivalences for ψ, ϑ, and π.