Sets of primes of Dirichlet density zero

For a number field K, Mathlib's NumberField.Set.HasDirichletDensity S δ says that P_S(s) / P(s) → δ as s → 1⁺, where P_S(s) = ∑_{𝔭 ∈ S} N(𝔭) ^ (-s) and P is the sum over all height-one primes. Since P(s) → ∞ as s → 1⁺ (TauCeti.tendsto_primeIdealZetaSum_univ_atTop), any set whose partial sum stays bounded near 1 has Dirichlet density zero. This covers every finite set of primes, and every set whose series ∑_{𝔭 ∈ S} N(𝔭)⁻¹ converges, such as the primes of residue degree greater than one.

A set of density zero is negligible: two sets whose symmetric difference has density zero have the same Dirichlet density, or neither has one. In particular the Dirichlet density of a set of primes does not change when finitely many primes are added or removed, or when the set is restricted to the primes of residue degree one.

Main results

• NumberField.Set.hasDirichletDensity_zero_of_eventually_le: a set whose partial sum is bounded as s → 1⁺ has Dirichlet density zero.
• NumberField.Set.hasDirichletDensity_zero_of_summable: a set of primes with ∑_{𝔭 ∈ S} N(𝔭)⁻¹ < ∞ has Dirichlet density zero.
• NumberField.Set.hasDirichletDensity_of_finite: a finite set of primes has Dirichlet density zero, so a set of nonzero Dirichlet density is infinite (NumberField.Set.HasDirichletDensity.infinite).
• NumberField.Set.hasDirichletDensity_iff_of_symmDiff: sets whose symmetric difference has density zero have the same densities; NumberField.Set.hasDirichletDensity_iff_of_finite_symmDiff is the case of a finite symmetric difference.
• TauCeti.hasDirichletDensity_higherDegreePrimes: the primes of residue degree greater than one have Dirichlet density zero, and TauCeti.hasDirichletDensity_inter_compl_higherDegreePrimes_iff lets a density be computed on the primes of residue degree one alone.

References

• J.-P. Serre, A Course in Arithmetic, Chapter VI, §4.1.
• J. Neukirch, Algebraic Number Theory, Chapter VII, §13.

theorem NumberField.Set.hasDirichletDensity_zero_of_eventually_le {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {C : ℝ} (h : ∀ᶠ (s : ℝ) in nhdsWithin 1 (Set.Ioi 1), primeIdealZetaSum S s ≤ C) : HasDirichletDensity S 0

A bounded partial sum gives density zero. If P_S(s) ≤ C for all s close enough to 1 from the right, then S has Dirichlet density zero, because the all-prime denominator tends to infinity.

theorem NumberField.Set.hasDirichletDensity_zero_of_summable {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} (h : Summable fun (𝔭 : ↑S) => ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-1)) : HasDirichletDensity S 0

A convergent reciprocal-norm series gives density zero. If ∑_{𝔭 ∈ S} N(𝔭)⁻¹ converges, then S has Dirichlet density zero: for s ≥ 1 every term N(𝔭) ^ (-s) is at most N(𝔭)⁻¹, so the partial sums stay bounded as s → 1⁺.

theorem NumberField.Set.hasDirichletDensity_of_finite {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} (hS : S.Finite) : HasDirichletDensity S 0

Finite sets of primes have Dirichlet density zero.

theorem NumberField.Set.HasDirichletDensity.infinite {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ : ℝ} (hS : HasDirichletDensity S δ) (hδ : δ ≠ 0) : S.Infinite

Sets of nonzero density are infinite. A set of primes with a nonzero Dirichlet density is infinite, because a finite set of primes has Dirichlet density zero.

theorem NumberField.Set.HasDirichletDensity.zero_of_subset {K : Type u_1} [Field K] [NumberField K] {S T : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} (hT : HasDirichletDensity T 0) (hST : S ⊆ T) : HasDirichletDensity S 0

Subsets of sets of density zero have density zero.

theorem NumberField.Set.HasDirichletDensity.of_symmDiff {K : Type u_1} [Field K] [NumberField K] {S T : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ : ℝ} (hT : HasDirichletDensity T δ) (h : HasDirichletDensity (symmDiff S T) 0) : HasDirichletDensity S δ

Sets of density zero are negligible. If T has Dirichlet density δ and the symmetric difference S ∆ T has Dirichlet density zero, then S has Dirichlet density δ.

theorem NumberField.Set.hasDirichletDensity_iff_of_symmDiff {K : Type u_1} [Field K] [NumberField K] {S T : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ : ℝ} (h : HasDirichletDensity (symmDiff S T) 0) : HasDirichletDensity S δ ↔ HasDirichletDensity T δ

Two sets of primes whose symmetric difference has Dirichlet density zero have the same Dirichlet densities.

theorem NumberField.Set.dirichletDensity_eq_of_symmDiff {K : Type u_1} [Field K] [NumberField K] {S T : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} (h : HasDirichletDensity (symmDiff S T) 0) : dirichletDensity S = dirichletDensity T

Two sets of primes whose symmetric difference has Dirichlet density zero have the same value of NumberField.Set.dirichletDensity, including when neither has a Dirichlet density.

theorem NumberField.Set.HasDirichletDensity.of_finite_symmDiff {K : Type u_1} [Field K] [NumberField K] {S T : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ : ℝ} (hT : HasDirichletDensity T δ) (hST : (symmDiff S T).Finite) : HasDirichletDensity S δ

Finite changes do not affect Dirichlet density. If T has Dirichlet density δ and S differs from T in finitely many primes, then S has Dirichlet density δ.

theorem NumberField.Set.hasDirichletDensity_iff_of_finite_symmDiff {K : Type u_1} [Field K] [NumberField K] {S T : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ : ℝ} (hST : (symmDiff S T).Finite) : HasDirichletDensity S δ ↔ HasDirichletDensity T δ

Two sets of primes differing in finitely many primes have the same Dirichlet densities.

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

The primes of residue degree greater than one have Dirichlet density zero, because their reciprocal-norm series converges.

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

The primes of residue degree one have Dirichlet density one.

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

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