The primes of residue degree above one are negligible

A height-one prime 𝔭 of 𝓞 K lies over a unique rational prime p, and its absolute norm is p ^ f for f the residue degree Ideal.inertiaDeg 𝔭.asIdeal ℤ. This file bounds the contribution of the primes with f ≥ 2, the set TauCeti.higherDegreePrimes K: they number O(√x) up to norm x, hence also o(x / log x), and their Dirichlet series ∑ N(𝔭) ^ (-s) converges for every s > 1/2, with a bound that is uniform on s ≥ 1.

Two elementary inputs carry the whole argument.

• A prime with f ≥ 2 has N(𝔭) = p ^ f ≥ p ^ 2, so it is not determined by a rational prime of size N(𝔭) but by one of size at most √(N(𝔭)).
• At most [K : ℚ] height-one primes lie over one rational prime, by the fundamental identity ∑ e f = [K : ℚ]; this is the already available TauCeti.card_filter_rationalPrimeBelow_le_finrank, itself resting on TauCeti.NumberField.card_primesOverFinset_le_finrank.

Together these compare any finite sum over the degree-above-one primes with [K : ℚ] times a sum over the rational primes with the exponent doubled, which is TauCeti.sum_absNorm_rpow_higherDegreePrimes_le_finrank_mul_tsum below. Counting gives the O(√x) bound, and summing m ^ (-2s) gives convergence for every s > 1/2 together with a bound on the partial Dirichlet series that is uniform on s ≥ 1.

Main results

• TauCeti.primeCount_higherDegreePrimes_le: the explicit count π_K(x; f ≥ 2) ≤ [K : ℚ] · √x, with TauCeti.primeCount_higherDegreePrimes_isBigO and TauCeti.primeCount_higherDegreePrimes_isLittleO its O(√x) and o(x / log x) forms.
• TauCeti.summable_absNorm_rpow_higherDegreePrimes: ∑ N(𝔭) ^ (-s) over the degree-above-one primes converges for every s > 1/2, in particular at s = 1.
• TauCeti.primeTheta_higherDegreePrimes_isLittleO: those primes carry weight o(x) in ϑ_K.
• TauCeti.primeIdealZetaSum_higherDegreePrimes_le: that sum, in Mathlib's NumberField.Set.primeIdealZetaSum vocabulary, is at most 2 [K : ℚ] for every s ≥ 1.
• TauCeti.sum_absNorm_rpow_le_finrank_mul_tsum and TauCeti.tsum_absNorm_rpow_le_finrank_mul_tsum: the same fibring over all height-one primes, in finite and infinite form, for every s > 1.
• TauCeti.tsum_absNorm_rpow_neg_two_le: at s = 2 that becomes the explicit ∑_𝔭 N(𝔭) ^ (-2) ≤ 2 [K : ℚ].

No density-zero statement is proved here. What this file supplies is the numerator half of one: NumberField.Set.HasDirichletDensity (higherDegreePrimes K) 0 asks for primeIdealZetaSum (higherDegreePrimes K) s / primeIdealZetaSum univ s → 0 as s → 1⁺, and the bound below controls only the numerator. Together with the divergence of the denominator it gives TauCeti.hasDirichletDensity_higherDegreePrimes in TauCeti.NumberTheory.ArithmeticDirichletSeries.DirichletDensity.Negligible. By contrast primeCount K (higherDegreePrimes K) =o[atTop] primeCount K univ would need a lower bound on the full prime count, which the prime ideal theorem supplies and which is not available here; the o(x / log x) statement below is against the explicit function x / log x, not against π_K.

Implementation notes

The set TauCeti.higherDegreePrimes and the map TauCeti.rationalPrimeBelow the estimates fibre over, together with their elementary norm and inertia theory, are algebraic rather than analytic and live in TauCeti.NumberTheory.NumberField.ResidueDegree.

References

• J. Neukirch, Algebraic Number Theory, Chapter VII, §13.
• J.-P. Serre, A Course in Arithmetic, Chapter VI, and J. Milne, Algebraic Number Theory, Chapter VIII, for the same estimate in the Dirichlet-density setting.

Fibring a sum over the rational primes below the primes

theorem TauCeti.sum_comp_rationalPrimeBelow_le {K : Type u_1} [Field K] [NumberField K] {g : ℕ → ℝ} {F : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {T : Finset ℕ} (hg : ∀ m ∈ T, 0 ≤ g m) (hFT : ∀ 𝔭 ∈ F, rationalPrimeBelow 𝔭 ∈ T) : ∑ 𝔭 ∈ F, g (rationalPrimeBelow 𝔭) ≤ ↑(Module.finrank ℚ K) * ∑ m ∈ T, g m

Comparison of a finite sum over height-one primes with a sum over the rational primes below them: the fibres have at most [K : ℚ] elements.

theorem TauCeti.sum_comp_rationalPrimeBelow_le_finrank_mul_tsum {K : Type u_1} [Field K] [NumberField K] {g : ℕ → ℝ} (hg : ∀ (m : ℕ), 0 ≤ g m) (hsum : Summable g) (F : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) : ∑ 𝔭 ∈ F, g (rationalPrimeBelow 𝔭) ≤ ↑(Module.finrank ℚ K) * ∑' (m : ℕ), g m

Comparison of a finite sum over height-one primes with the whole sum over ℕ: fibring costs a factor [K : ℚ], and completing the finite rational-prime sum to its tsum costs nothing because the summand is nonnegative. This is the shape both norm-sum bounds below take, once each has compared its own summand termwise with g (rationalPrimeBelow 𝔭).

Counting the primes of residue degree above one

theorem TauCeti.primeCount_higherDegreePrimes_le {K : Type u_1} [Field K] [NumberField K] (x : ℝ) : primeCount K (higherDegreePrimes K) x ≤ ↑(Module.finrank ℚ K) * √x

There are at most [K : ℚ] √x primes of residue degree above one and norm at most x: each lies over a rational prime of size at most √x, and at most [K : ℚ] of them lie over the same one.

theorem TauCeti.primeCount_higherDegreePrimes_isBigO {K : Type u_1} [Field K] [NumberField K] : primeCount K (higherDegreePrimes K) =O[Filter.atTop] Real.sqrt

The primes of residue degree above one and norm at most x number O(√x).

theorem TauCeti.primeCount_higherDegreePrimes_isLittleO {K : Type u_1} [Field K] [NumberField K] : primeCount K (higherDegreePrimes K) =o[Filter.atTop] fun (x : ℝ) => x / Real.log x

The primes of residue degree above one and norm at most x number o(x / log x). The comparison is with the explicit function x / log x, not with the full prime count π_K(x); combined with the prime ideal theorem π_K(x) ~ x / log x it gives natural density zero, TauCeti.hasNaturalDensity_higherDegreePrimes.

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

The primes of residue degree above one carry a negligible weight. Their contribution to ϑ_K is o(x).

This is the count o(x / log x) above, weighted by Chebyshev's log x per prime. It is the estimate a contraction between two number fields discards: the norms satisfy 𝔑_{E/ℚ}𝔓 = (𝔑_{K/ℚ}𝔭)^{f(𝔓/𝔭)}, so a term of ϑ moves to a different value of n unless the relative residue degree is one, and f(𝔓/𝔭) ≥ 2 forces f(𝔓/p) ≥ 2, which is what this absolute statement covers.

Convergence of the prime Dirichlet series over the degree-above-one primes

theorem TauCeti.sum_absNorm_rpow_higherDegreePrimes_le_finrank_mul_tsum {K : Type u_1} [Field K] [NumberField K] {s : ℝ} (hs : 1 / 2 < s) {F : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (hF : ∀ 𝔭 ∈ F, 𝔭 ∈ higherDegreePrimes K) : ∑ 𝔭 ∈ F, ↑(Ideal.absNorm 𝔭.asIdeal) ^ (-s) ≤ ↑(Module.finrank ℚ K) * ∑' (m : ℕ), ↑m ^ (-(2 * s))

The key comparison: a finite sum of N(𝔭) ^ (-s) over primes of residue degree above one is bounded by [K : ℚ] times the full sum of m ^ (-2s) over the natural numbers.

theorem TauCeti.summable_absNorm_rpow_higherDegreePrimes {K : Type u_1} [Field K] [NumberField K] {s : ℝ} (hs : 1 / 2 < s) : Summable fun (𝔭 : ↑(higherDegreePrimes K)) => ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s)

The Dirichlet series over the primes of residue degree above one converges for every s > 1/2, in particular at s = 1.

theorem TauCeti.primeIdealZetaSum_higherDegreePrimes_le {K : Type u_1} [Field K] [NumberField K] {s : ℝ} (hs : 1 ≤ s) : NumberField.Set.primeIdealZetaSum (higherDegreePrimes K) s ≤ 2 * ↑(Module.finrank ℚ K)

Uniformly in s ≥ 1, the partial Dirichlet sum over the primes of residue degree above one is at most 2 [K : ℚ]. This bounds the numerator of NumberField.Set.HasDirichletDensity as s → 1⁺; it is one half of Dirichlet density zero, the other half being the divergence of the all-prime denominator.

All height-one primes

theorem TauCeti.sum_absNorm_rpow_le_finrank_mul_tsum {K : Type u_1} [Field K] [NumberField K] {s : ℝ} (hs : 1 < s) (F : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) : ∑ 𝔭 ∈ F, ↑(Ideal.absNorm 𝔭.asIdeal) ^ (-s) ≤ ↑(Module.finrank ℚ K) * ∑' (m : ℕ), ↑m ^ (-s)

A finite norm sum is at most [K : ℚ] times the sum of m ^ (-s) over ℕ. Fibring a finite sum of N(𝔭) ^ (-s) over the rational primes below costs a factor [K : ℚ]. Without a residue-degree hypothesis only p ≤ N(𝔭) is available, so the exponent stays -s and the argument needs 1 < s; the degree-above-one analogue TauCeti.sum_absNorm_rpow_higherDegreePrimes_le_finrank_mul_tsum gains the exponent -2s and so reaches down to s > 1/2.

theorem TauCeti.tsum_absNorm_rpow_le_finrank_mul_tsum {K : Type u_1} [Field K] [NumberField K] {s : ℝ} (hs : 1 < s) : ∑' (𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), ↑(Ideal.absNorm 𝔭.asIdeal) ^ (-s) ≤ ↑(Module.finrank ℚ K) * ∑' (m : ℕ), ↑m ^ (-s)

The prime ideal zeta sum is at most [K : ℚ] times the sum of m ^ (-s) over ℕ. The finite-sum comparison passes to the limit on the whole range 1 < s where both sides converge. Specializing the exponent is what buys an explicit constant, as in TauCeti.tsum_absNorm_rpow_neg_two_le.

theorem TauCeti.tsum_absNorm_rpow_neg_two_le {K : Type u_1} [Field K] [NumberField K] : ∑' (𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), ↑(Ideal.absNorm 𝔭.asIdeal) ^ (-2) ≤ 2 * ↑(Module.finrank ℚ K)

The prime ideal zeta sum over all height-one primes at s = 2 is at most 2 [K : ℚ]. At most [K : ℚ] primes lie over each rational prime, and ζ (2) < 2. The same constant bounds the degree-above-one primes for every s ≥ 1: TauCeti.primeIdealZetaSum_higherDegreePrimes_le. The constant is available only from s = 2 upwards: at s just above 1 the sum over ℕ is already larger than 2, so only the s-dependent bound above survives there.