Natural density of primes of residue degree greater than one

The O(√x) bound for primes of residue degree greater than one, proved in TauCeti.NumberTheory.ArithmeticDirichletSeries.ResidueDegree, is o(x / log x). The prime ideal theorem then shows that these primes have natural density zero. Their complement has density one, and removing them preserves any natural density.

For Dirichlet density of prime ideals in number fields, see J. Neukirch, Algebraic Number Theory, Chapter VII, §13.

theorem TauCeti.hasNaturalDensity_higherDegreePrimes {K : Type u_1} [Field K] [NumberField K] : NumberField.Set.HasNaturalDensity (higherDegreePrimes K) 0

The primes of residue degree greater than one have natural density zero: there are O(√x) of them of norm at most x, which is o(x / log x).

theorem TauCeti.hasNaturalDensity_compl_higherDegreePrimes {K : Type u_1} [Field K] [NumberField K] : NumberField.Set.HasNaturalDensity (higherDegreePrimes K)ᶜ 1

The primes of residue degree one have natural density one.

theorem TauCeti.hasNaturalDensity_inter_compl_higherDegreePrimes_iff {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {δ : ℝ} : NumberField.Set.HasNaturalDensity (S ∩ (higherDegreePrimes K)ᶜ) δ ↔ NumberField.Set.HasNaturalDensity S δ

Natural density only sees primes of residue degree one. A set S of primes has natural density δ if and only if its primes of residue degree one do.