Natural density of sets of prime ideals

For a number field K, this file defines the natural density of a set S of nonzero prime ideals as the limit

  primeCount K S x / primeCount K Set.univ x

as the inclusive real cutoff x tends to infinity. This normalization matches Mathlib's ratio-normalized NumberField.Set.HasDirichletDensity: a density is measured relative to all prime ideals of the same number field, rather than relative to an external approximation such as x / log x.

The denominator really tends to infinity. Indeed, lying over supplies a prime of 𝓞 K above every rational prime, so the height-one spectrum is infinite. Its bounded-norm subsets are finite and exhaust the spectrum, whence their cardinalities tend to infinity. This fact both makes the whole spectrum have density one and ensures that a fixed finite error disappears in the ratio. More generally, a set of density zero can be added or removed without changing a natural density.

Comparison with x / log x is a theorem rather than the definition. The prime ideal theorem π_K(x) ~ x / log x (TauCeti.primeCount_univ_isEquivalent_div_log) shows that S has natural density δ exactly when π_S(x) / (x / log x) → δ, equivalently when π_S(x) = δ Li(x) + o(x / log x).

Main results

• NumberField.Set.HasNaturalDensity: ratio-normalized natural density for a set of prime ideals.
• NumberField.Set.hasNaturalDensity_def: the defining ratio-convergence characterization.
• NumberField.Set.HasNaturalDensity.union, NumberField.Set.hasNaturalDensity_biUnion_finset and NumberField.Set.HasNaturalDensity.compl: finite Boolean calculus for natural density.
• NumberField.Set.hasNaturalDensity_of_finite: every finite set of prime ideals has natural density zero.
• NumberField.Set.hasNaturalDensity_iff_of_symmDiff: two prime sets whose symmetric difference has natural density zero have the same natural densities; NumberField.Set.hasNaturalDensity_iff_of_finite_symmDiff is the case of a finite symmetric difference.
• NumberField.Set.hasNaturalDensity_iff_tendsto_div_div_log and NumberField.Set.hasNaturalDensity_iff_isLittleO_logIntegral: S has natural density δ if and only if π_S(x) / (x / log x) → δ, if and only if π_S(x) = δ Li(x) + o(x / log x).
• NumberField.Set.hasNaturalDensity_zero_iff_isLittleO: S has natural density zero if and only if π_S(x) = o(x / log x).
• NumberField.Set.isUpperDirichletDensityBound_of_eventually_primeCount_le and NumberField.Set.isLowerDirichletDensityBound_of_eventually_le_primeCount: an eventual one-sided bound on the proportion of primes of S below x is the same one-sided bound for Dirichlet density.
• NumberField.Set.hasDirichletDensity_of_hasNaturalDensity: natural density implies Dirichlet density, with the same value.

The comparison with Dirichlet density rests on two inputs. Abel summation against the decreasing function t ↦ t ^ (-s) (TauCeti.tsum_mul_le_of_summatory_le) turns an eventual bound π_S(x) ≤ c · π(x) into a bound P_S(s) ≤ c · P(s) + C with C independent of s > 1, where P_S is Mathlib's NumberField.Set.primeIdealZetaSum S. The all-prime sum P(s) tends to infinity as s → 1⁺ (TauCeti.tendsto_primeIdealZetaSum_univ_atTop), so the constant C disappears from the ratio P_S(s) / P(s).

For the natural and Dirichlet densities of rational primes and the implication from natural to Dirichlet density, see J.-P. Serre, A Course in Arithmetic, Chapter VI, §4.5. For Dirichlet density of prime ideals in number fields, see J. Neukirch, Algebraic Number Theory, Chapter VII, §13.

def NumberField.Set.HasNaturalDensity {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) (δ : ℝ) : Prop

A set S of height-one primes of a number field has natural density δ when the proportion of primes of S below x, relative to all primes below x, tends to δ as x → ∞.

Both counts use the inclusive real cutoff fixed by TauCeti.primeCount.

Equations

• NumberField.Set.HasNaturalDensity S δ = Filter.Tendsto (fun (x : ℝ) => TauCeti.primeCount K S x / TauCeti.primeCount K Set.univ x) Filter.atTop (nhds δ)

theorem NumberField.Set.hasNaturalDensity_def {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ : ℝ} : HasNaturalDensity S δ ↔ Filter.Tendsto (fun (x : ℝ) => TauCeti.primeCount K S x / TauCeti.primeCount K Set.univ x) Filter.atTop (nhds δ)

Unfolds HasNaturalDensity to the convergence of the ratio of prime counts.

theorem NumberField.Set.HasNaturalDensity.unique {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ ε : ℝ} (hδ : HasNaturalDensity S δ) (hε : HasNaturalDensity S ε) : δ = ε

A set of prime ideals has at most one natural density.

@[simp]

theorem NumberField.Set.hasNaturalDensity_empty {K : Type u_1} [Field K] [NumberField K] : HasNaturalDensity ∅ 0

The empty set of prime ideals has natural density zero.

@[simp]

theorem NumberField.Set.hasNaturalDensity_univ {K : Type u_1} [Field K] [NumberField K] : HasNaturalDensity Set.univ 1

The set of all prime ideals has natural density one.

theorem NumberField.Set.HasNaturalDensity.nonneg {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ : ℝ} (h : HasNaturalDensity S δ) : 0 ≤ δ

A natural density is nonnegative.

theorem NumberField.Set.HasNaturalDensity.le_one {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ : ℝ} (h : HasNaturalDensity S δ) : δ ≤ 1

A natural density is at most one.

theorem NumberField.Set.HasNaturalDensity.mono {K : Type u_1} [Field K] [NumberField K] {S T : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ ε : ℝ} (hST : S ⊆ T) (hS : HasNaturalDensity S δ) (hT : HasNaturalDensity T ε) : δ ≤ ε

Inclusion of prime sets orders their natural densities, when both densities exist.

theorem NumberField.Set.HasNaturalDensity.union {K : Type u_1} [Field K] [NumberField K] {S T : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ ε : ℝ} (hS : HasNaturalDensity S δ) (hT : HasNaturalDensity T ε) (hST : Disjoint S T) : HasNaturalDensity (S ∪ T) (δ + ε)

Natural density is additive on disjoint unions of prime sets.

theorem NumberField.Set.hasNaturalDensity_biUnion_finset {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} {s : Finset ι} {f : ι → Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {d : ι → ℝ} (hf : ∀ i ∈ s, HasNaturalDensity (f i) (d i)) (hdisj : (↑s).PairwiseDisjoint f) : HasNaturalDensity (⋃ i ∈ s, f i) (∑ i ∈ s, d i)

Natural density is additive on a finite family of pairwise disjoint prime sets.

theorem NumberField.Set.HasNaturalDensity.compl {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ : ℝ} (hS : HasNaturalDensity S δ) : HasNaturalDensity Sᶜ (1 - δ)

The complement of a set of natural density δ has natural density 1 - δ.

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

Every finite set of prime ideals has natural density zero: its count is eventually constant, while the all-prime count tends to infinity.

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

A set of prime ideals with nonzero natural density is infinite.

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

Every subset of a set of natural density zero has natural density zero.

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

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

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

Two prime sets whose symmetric difference has natural density zero have natural density δ simultaneously.

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

Changing a set on finitely many prime ideals preserves its natural density.

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

Two prime sets with finite symmetric difference have natural density δ simultaneously.

Natural density implies Dirichlet density

theorem NumberField.Set.isUpperDirichletDensityBound_of_eventually_primeCount_le {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {c : ℝ} (h : ∀ᶠ (x : ℝ) in Filter.atTop, TauCeti.primeCount K S x ≤ c * TauCeti.primeCount K Set.univ x) : IsUpperDirichletDensityBound S c

Upper natural bounds are upper Dirichlet bounds. If eventually at most the proportion c of the primes of norm at most x lie in S, then c is an upper Dirichlet-density bound for S.

theorem NumberField.Set.isLowerDirichletDensityBound_of_eventually_le_primeCount {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {c : ℝ} (h : ∀ᶠ (x : ℝ) in Filter.atTop, c * TauCeti.primeCount K Set.univ x ≤ TauCeti.primeCount K S x) : IsLowerDirichletDensityBound S c

Lower natural bounds are lower Dirichlet bounds. If eventually at least the proportion c of the primes of norm at most x lie in S, then c is a lower Dirichlet-density bound for S.

theorem NumberField.Set.hasDirichletDensity_of_hasNaturalDensity {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ : ℝ} (h : HasNaturalDensity S δ) : HasDirichletDensity S δ

Natural density implies Dirichlet density. A set of prime ideals with natural density δ has Dirichlet density δ.

Comparison with x / log x

theorem NumberField.Set.hasNaturalDensity_iff_tendsto_div_div_log {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ : ℝ} : HasNaturalDensity S δ ↔ Filter.Tendsto (fun (x : ℝ) => TauCeti.primeCount K S x / (x / Real.log x)) Filter.atTop (nhds δ)

Natural density against x / log x. By the prime ideal theorem the all-prime count is asymptotic to x / log x, so a set S of prime ideals has natural density δ exactly when π_S(x) / (x / log x) → δ.

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

Natural density from prime counting against the logarithmic integral. A set S of prime ideals has natural density δ exactly when π_S(x) = δ Li(x) + o(x / log x).

theorem NumberField.Set.hasNaturalDensity_zero_iff_isLittleO {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} : HasNaturalDensity S 0 ↔ TauCeti.primeCount K S =o[Filter.atTop] fun (x : ℝ) => x / Real.log x

Natural density zero. A set S of prime ideals has natural density zero exactly when π_S(x) = o(x / log x).