From the weighted prime count to the unweighted one

A prime-number-theorem argument delivers its conclusion for a logarithmically weighted count: a Tauberian theorem applied to a logarithmic derivative sees the von Mangoldt coefficients, hence the count ψ weighted by log p and taken over prime powers, and a separate elementary estimate for the prime-power contribution passes from ψ to the count ϑ over primes alone. The statement one wants is about the unweighted count π. This file carries out that last passage for the primes of a number field, taking the asymptotic for ϑ as given: if ϑ(x) = δx + o(x), then π(x) = δ Li(x) + o(x/log x), where Li is the offset logarithmic integral of TauCeti/Analysis/SpecialFunctions/LogIntegral.lean.

The bridge is the exact Abel-summation identity TauCeti.primeCount_eq_primeTheta_div_log_add_integral of Layer 6.1 together with the antiderivative identity TauCeti.Real.logIntegral_eq_div_log_sub_add for Li. Subtracting the two cancels the main terms and leaves TauCeti.primeCount_sub_mul_logIntegral_eq, an identity valid for every x ≥ 2 and every δ, whose three remaining summands are each o (x / log x).

Main results

• TauCeti.primeCount_sub_mul_logIntegral_eq: the exact identity π(x) - δ Li(x) = (ϑ(x) - δx)/log x + ∫ t in 2..x, (ϑ(t) - δt)/(t log² t) + 2δ/log 2.
• TauCeti.primeCount_sub_mul_logIntegral_isLittleO: the transfer itself, stated so that it covers the density δ = 0 as well.
• TauCeti.primeCount_asymptotic_of_primeTheta: the quotient form ϑ(x) ∼ δx ⟹ π(x) ∼ δ Li(x) for δ ≠ 0, and TauCeti.primeCount_isLittleO_logIntegral for the zero-density case, where an asymptotic equivalence would be false and the correct statement is π(x) = o(Li x).

Roadmap role

This is Layer 6.2 of TauCetiRoadmap/ArithmeticDirichletSeries/README.md, which asks for the transfer ϑ(x) ∼ δx ⟹ π(x) ∼ δ Li(x) "including the zero-density and δ = 0 cases"; Layer 10.3 exports it as primeCount_asymptotic_of_primeTheta. Nothing here uses an analytic continuation or a nonvanishing statement: the hypothesis on ϑ is taken as given here, and Layer 10 supplies it.

References

• H. Davenport, Multiplicative Number Theory, Chapter 1.
• G. Tenenbaum, Introduction to Analytic and Probabilistic Number Theory, Chapter I.2.

Mathlib's Chebyshev.primeCounting_sub_theta_div_log_isBigO performs the same partial-summation step for the rational primes; the argument below follows it, and replaces its explicit Chebyshev bound by the hypothesis on ϑ.

theorem TauCeti.intervalIntegrable_primeTheta_sub_const_mul {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (δ a b : ℝ) : IntervalIntegrable (fun (t : ℝ) => primeTheta K S t - δ * t) MeasureTheory.volume a b

The error term ϑ(t) - δ t is interval integrable: ϑ is monotone and t ↦ δ t is continuous.

theorem TauCeti.primeCount_sub_mul_logIntegral_eq {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (δ : ℝ) {x : ℝ} (hx : 2 ≤ x) : primeCount K S x - δ * Real.logIntegral x = ((primeTheta K S x - δ * x) / Real.log x + ∫ (t : ℝ) in 2..x, (primeTheta K S t - δ * t) / (t * Real.log t ^ 2)) + 2 * δ / Real.log 2

The exact remainder identity. Subtracting δ Li(x) from the Abel-summation formula for π(x) cancels the two x / log x main terms and leaves a boundary quotient, an integral against (t log² t)⁻¹ of the same error term, and the constant coming from the base point 2 of Li.

The identity holds for every real δ; no hypothesis relating ϑ and δ is used.

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

The transfer from ϑ to π. If the logarithmically weighted count of the primes of S satisfies ϑ(x) = δx + o(x), then the unweighted count satisfies π(x) = δ Li(x) + o(x/log x).

Stated with an error term rather than as an equivalence, this covers δ = 0 as well; the two quotient forms are TauCeti.primeCount_asymptotic_of_primeTheta and TauCeti.primeCount_isLittleO_logIntegral.

theorem TauCeti.primeCount_isLittleO_logIntegral {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (h : primeTheta K S =o[Filter.atTop] id) : primeCount K S =o[Filter.atTop] Real.logIntegral

The zero-density case. If the logarithmically weighted count of S is o(x), then S contains o(Li x) primes up to x. An asymptotic equivalence is not the right statement here: π ~ 0 would force π to vanish eventually.

theorem TauCeti.primeCount_asymptotic_of_primeTheta {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {δ : ℝ} (hδ : δ ≠ 0) (h : Asymptotics.IsEquivalent Filter.atTop (primeTheta K S) fun (x : ℝ) => δ * x) : Asymptotics.IsEquivalent Filter.atTop (primeCount K S) fun (x : ℝ) => δ * Real.logIntegral x

ϑ(x) ∼ δx implies π(x) ∼ δ Li(x), for a nonzero density δ. This is the transfer the prime-number-theorem chain consumes: Layer 10 produces the asymptotic for ϑ from a Tauberian theorem, and this turns it into one for π.