Crude prime counts and the higher prime powers of a number field

Chebyshev's ψ counts every prime power 𝔭 ^ k with the logarithmic weight log N(𝔭), while ϑ counts only the primes themselves. Their difference is the sum of log N(𝔭) over the higher prime powers, those with k ≥ 2, and the point of this file is that this difference is negligible: it is O(√x log² x), hence o(x).

Two elementary counting bounds carry the argument.

• TauCeti.two_pow_card_le_absNorm: distinct primes dividing a nonzero ideal I each contribute a factor of at least 2 to N(I), so there are at most log₂ N(I) of them.
• TauCeti.card_primesLE_mul_log_two_le: every prime of norm at most x divides the principal ideal generated by ⌊x⌋₊ !, whose absolute norm is (⌊x⌋₊ !) ^ [K:ℚ]. Feeding that into the previous bound gives π_K(x) ≤ [K:ℚ] / log 2 · x log x.

Neither bound is sharp — the true order of π_K(x) is x / log x — but they are proved from scratch, with no analytic input and an explicit constant, and they are strong enough for every estimate below. The repository's existing effective count NumberField.card_ideal_absNorm_le, which bounds the number of nonzero ideals of norm at most X by X² · 2 ^ [K:ℚ], is not: being quadratic it only gives π_K(√x) = O(x), which loses the saving that makes the higher prime powers negligible.

The higher prime powers are then summed by fibring over the prime base: for a fixed prime 𝔭, the exponents k ≥ 2 with N(𝔭) ^ k ≤ x number at most log x / log N(𝔭), so the whole fibre contributes at most log x. Since a higher prime power of norm at most x has N(𝔭) ^ 2 ≤ x, only the primes of norm at most √x occur, and the total is at most π_K(√x) · log x.

Main definitions

• TauCeti.higherPrimePowerWeight is the standard logarithmic prime-power weight log N(𝔭), restricted to the prime powers 𝔭 ^ k with k ≥ 2 and set to zero on the primes themselves.
• TauCeti.higherPrimePowerTheta is its inclusive summatory function, that is, ψ - ϑ.

Main results

• TauCeti.primeCount_le_mul_log and TauCeti.primeCount_isBigO: the crude prime count.
• TauCeti.higherPrimePowerTheta_le: the explicit bound ψ(x) - ϑ(x) ≤ [K:ℚ] / (2 log 2) · √x log² x.
• TauCeti.higherPrimePowerTheta_isBigO and TauCeti.higherPrimePowerTheta_isLittleO: the O(√x log² x) and o(x) forms.
• TauCeti.primePowerSummatory_isLittleO_of_le_higherPrimePowerWeight: the same conclusion for any normed additive-group-valued prime-power weight whose norm is dominated by a constant multiple of the standard one. This isolates exactly the hypothesis another arithmetic weight has to supply.
• TauCeti.primePowerSummatory_indicator_isLittleO: its specialization to the higher prime powers whose base lies in a prescribed set of primes.

Roadmap role

This is the prime and prime-power half of Layer 5.1 together with Layer 5.2 of TauCetiRoadmap/ArithmeticDirichletSeries/README.md, whose target 5.2 asks for "the generic O(√x log² x) estimate under the standard logarithmic prime-power weight" and for the hypotheses needed by other arithmetic weights. Layer 10.2 consumes it as the named estimate turning an asymptotic for ψ into one for ϑ; the roadmap's own accounting there requires only the o(x) corollary.

The ideal-counting half of Layer 5.1 is a separate estimate: it is analytic, resting on Mathlib's NumberField.Ideal.tendsto_norm_le_div_atTop₀, and is not needed here.

References

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

Counting the primes below a cutoff

theorem TauCeti.two_pow_card_le_absNorm {K : Type u_1} [Field K] [NumberField K] {I : Ideal (NumberField.RingOfIntegers K)} (hI : I ≠ 0) {s : Finset (Ideal (NumberField.RingOfIntegers K))} (hprime : ∀ P ∈ s, Prime P) (hdvd : ∀ P ∈ s, P ∣ I) : 2 ^ s.card ≤ Ideal.absNorm I

Distinct primes dividing a nonzero ideal I each contribute a factor of at least 2 to N(I), so I has at most log₂ N(I) distinct prime divisors.

theorem TauCeti.card_primesLE_mul_log_two_le (K : Type u_2) [Field K] [NumberField K] {x : ℝ} (hx : 1 ≤ x) : ↑(primesLE K x).card * Real.log 2 ≤ ↑(Module.finrank ℚ K) * (x * Real.log x)

The crude prime count: there are at most [K:ℚ] / log 2 · x log x height-one primes of absolute norm at most x.

Every such prime divides the ideal generated by ⌊x⌋₊ !, because a nonzero ideal contains its own absolute norm; that ideal has absolute norm (⌊x⌋₊ !) ^ [K:ℚ] ≤ (⌊x⌋₊ ^ ⌊x⌋₊) ^ [K:ℚ], and TauCeti.two_pow_card_le_absNorm converts this into a bound on the number of divisors.

theorem TauCeti.primeCount_le_card_primesLE {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (x : ℝ) : primeCount K S x ≤ ↑(primesLE K x).card

The count of any set of primes is at most the number of primes below the cutoff.

theorem TauCeti.primeCount_le_mul_log {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) {x : ℝ} (hx : 1 ≤ x) : primeCount K S x ≤ ↑(Module.finrank ℚ K) / Real.log 2 * (x * Real.log x)

The crude prime count, stated for the Layer 4 counting function TauCeti.primeCount.

theorem TauCeti.primeCount_isBigO {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) : primeCount K S =O[Filter.atTop] fun (x : ℝ) => x * Real.log x

The number of primes of norm at most x is O(x log x).

The standard logarithmic weight on the higher prime powers

noncomputable def TauCeti.higherPrimePowerWeight {K : Type u_1} [Field K] [NumberField K] (A : IdealPrimePower K) : ℝ

The standard logarithmic weight on the higher prime powers: the value log N(𝔭) on a prime power 𝔭 ^ k with k ≥ 2, and zero on the primes themselves.

Its summatory function is the difference between Chebyshev's ψ, which weights every prime power, and ϑ, which weights only the primes; Layer 10 defines ψ itself.

Equations

• TauCeti.higherPrimePowerWeight A = if 2 ≤ TauCeti.primePowerExponent A then Real.log ↑(Ideal.absNorm (TauCeti.primePowerBase A).asIdeal) else 0

@[simp]

theorem TauCeti.higherPrimePowerWeight_of_two_le_primePowerExponent {K : Type u_1} [Field K] [NumberField K] {A : IdealPrimePower K} (hA : 2 ≤ primePowerExponent A) : higherPrimePowerWeight A = Real.log ↑(Ideal.absNorm (primePowerBase A).asIdeal)

On a higher prime power, the standard weight is the logarithm of the norm of the base.

@[simp]

theorem TauCeti.higherPrimePowerWeight_of_prime {K : Type u_1} [Field K] [NumberField K] {A : IdealPrimePower K} (hA : Prime ↑↑A) : higherPrimePowerWeight A = 0

On a prime, the standard weight vanishes.

theorem TauCeti.higherPrimePowerWeight_nonneg {K : Type u_1} [Field K] [NumberField K] (A : IdealPrimePower K) : 0 ≤ higherPrimePowerWeight A

The higher-prime-power weight is nonnegative.

@[simp]

theorem TauCeti.higherPrimePowerWeight_eq_zero_iff {K : Type u_1} [Field K] [NumberField K] (A : IdealPrimePower K) : higherPrimePowerWeight A = 0 ↔ Prime ↑↑A

The higher-prime-power weight vanishes exactly on the primes.

theorem TauCeti.higherPrimePowerWeight_eq_vonMangoldt_re {K : Type u_1} [Field K] [NumberField K] {A : IdealPrimePower K} (hA : ¬Prime ↑↑A) : higherPrimePowerWeight A = (IdealArithmeticFunction.vonMangoldt ↑A).re

Away from the primes, the higher-prime-power weight is the ideal von Mangoldt function of Layer 2, whose values are real.

noncomputable def TauCeti.higherPrimePowerTheta (K : Type u_2) [Field K] [NumberField K] (x : ℝ) : ℝ

The inclusive summatory function of the higher-prime-power weight: the whole contribution of the exponents k ≥ 2 to Chebyshev's ψ.

Equations

• TauCeti.higherPrimePowerTheta K x = TauCeti.primePowerSummatory K TauCeti.higherPrimePowerWeight x

@[simp]

theorem TauCeti.higherPrimePowerTheta_apply (K : Type u_2) [Field K] [NumberField K] (x : ℝ) : higherPrimePowerTheta K x = primePowerSummatory K higherPrimePowerWeight x

The higher-prime-power theta function is the summatory function of the standard weight.

theorem TauCeti.higherPrimePowerTheta_nonneg (K : Type u_2) [Field K] [NumberField K] (x : ℝ) : 0 ≤ higherPrimePowerTheta K x

The higher-prime-power sum is nonnegative.

theorem TauCeti.higherPrimePowerTheta_mono (K : Type u_2) [Field K] [NumberField K] : Monotone (higherPrimePowerTheta K)

The higher-prime-power sum is monotone in the inclusive cutoff.

The O(√x log² x) estimate

theorem TauCeti.higherPrimePowerTheta_le_card_primesLE_mul_log (K : Type u_2) [Field K] [NumberField K] {x : ℝ} (hx : 1 ≤ x) : higherPrimePowerTheta K x ≤ ↑(primesLE K √x).card * Real.log x

Fibring the higher prime powers over their prime base: for a fixed prime 𝔭, the exponents k ≥ 2 with N(𝔭) ^ k ≤ x contribute at most log x in total, and only primes of norm at most √x occur at all.

theorem TauCeti.higherPrimePowerTheta_le (K : Type u_2) [Field K] [NumberField K] {x : ℝ} (hx : 1 ≤ x) : higherPrimePowerTheta K x ≤ ↑(Module.finrank ℚ K) / (2 * Real.log 2) * (√x * Real.log x ^ 2)

The higher prime powers are negligible, with an explicit constant: ψ(x) - ϑ(x) ≤ [K:ℚ] / (2 log 2) · √x log² x for x ≥ 1.

theorem TauCeti.higherPrimePowerTheta_isBigO (K : Type u_2) [Field K] [NumberField K] : higherPrimePowerTheta K =O[Filter.atTop] fun (x : ℝ) => √x * Real.log x ^ 2

The higher-prime-power sum is O(√x log² x); this is Layer 5.2's estimate.

theorem TauCeti.isLittleO_sqrt_mul_log_sq : (fun (x : ℝ) => √x * Real.log x ^ 2) =o[Filter.atTop] fun (x : ℝ) => x

√x log² x is o(x): this is what makes the higher prime powers negligible for the prime-number-theorem transfer of Layer 10.2.

theorem TauCeti.higherPrimePowerTheta_isLittleO (K : Type u_2) [Field K] [NumberField K] : higherPrimePowerTheta K =o[Filter.atTop] fun (x : ℝ) => x

The higher-prime-power sum is o(x).

Other arithmetic weights

theorem TauCeti.primePowerSummatory_isBigO_of_le_higherPrimePowerWeight (K : Type u_2) [Field K] [NumberField K] {E : Type u_3} [NormedAddCommGroup E] {w : IdealPrimePower K → E} {C : ℝ} (hC : 0 ≤ C) (hw : ∀ (A : IdealPrimePower K), ‖w A‖ ≤ C * higherPrimePowerWeight A) : (fun (x : ℝ) => primePowerSummatory K w x) =O[Filter.atTop] fun (x : ℝ) => √x * Real.log x ^ 2

The hypothesis another arithmetic weight has to supply: domination of its norm by a constant multiple of the standard logarithmic weight on the higher prime powers. This is an inequality on the weight alone, with no reference to any Euler product.

theorem TauCeti.primePowerSummatory_isLittleO_of_le_higherPrimePowerWeight (K : Type u_2) [Field K] [NumberField K] {E : Type u_3} [NormedAddCommGroup E] {w : IdealPrimePower K → E} {C : ℝ} (hC : 0 ≤ C) (hw : ∀ (A : IdealPrimePower K), ‖w A‖ ≤ C * higherPrimePowerWeight A) : (fun (x : ℝ) => primePowerSummatory K w x) =o[Filter.atTop] fun (x : ℝ) => x

Any normed additive-group-valued prime-power weight whose norm is dominated by a constant multiple of the standard logarithmic weight on the higher prime powers has o(x) summatory function.

theorem TauCeti.primePowerSummatory_indicator_isLittleO (K : Type u_2) [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) : (fun (x : ℝ) => primePowerSummatory K ({A : IdealPrimePower K | primePowerBase A ∈ S}.indicator higherPrimePowerWeight) x) =o[Filter.atTop] fun (x : ℝ) => x

Restricting to the prime powers whose base lies in a set S of primes only removes nonnegative terms, so the o(x) estimate survives. This is the form Layer 10.2 consumes when it removes the higher prime powers from ψ over a prime set.