Documentation

TauCeti.NumberTheory.ArithmeticDirichletSeries.DirichletDensity.Basic

The Boolean calculus of Dirichlet density #

For a number field K, Mathlib's NumberField.Set.HasDirichletDensity S δ says that

S.primeIdealZetaSum s / Set.univ.primeIdealZetaSum s → δ as s → 1⁺.

This file proves the elementary calculus of this predicate: uniqueness, the value 1 on all primes, monotonicity, additivity on finite disjoint unions, complements, and two squeezes. The first squeezes a set between two sets of the same density. The second is the finite-partition squeeze: given a finite pairwise disjoint family whose union has δ as an upper density bound, lower bounds on every member that already sum to δ leave no room, so each member's density is exactly its bound. It also shows that one-sided density bounds move along inclusions of sets, which is what makes the first squeeze work; the second rests instead on splitting the union's ratio exactly and spending the summed lower bounds against it.

All of these are statements about the ratio for s close to 1 from the right, and on that side both inputs they need are available: for 1 < s each partial sum is a genuine sum rather than the tsum junk value (TauCeti.summable_absNorm_rpow_subtype_of_one_lt), and the all-prime denominator is positive (NumberField.Set.primeIdealZetaSum_univ_pos_of_one_lt). In particular nothing here uses the divergence of the all-prime sum at s = 1. That divergence is what makes a finite set of primes have density zero; the finite-error statements that use it are in TauCeti.NumberTheory.ArithmeticDirichletSeries.DirichletDensity.Negligible.

Main results #

References #

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

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

source
@[simp]
theorem NumberField.Set.hasDirichletDensity_univ {K : Type u_1} [Field K] [NumberField K] :
HasDirichletDensity Set.univ 1

The set of all prime ideals has Dirichlet density one.

source
@[simp]
theorem NumberField.Set.dirichletDensity_univ {K : Type u_1} [Field K] [NumberField K] :
dirichletDensity Set.univ = 1

The Dirichlet density of the set of all prime ideals is one.

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

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

source
theorem NumberField.Set.hasDirichletDensity_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, HasDirichletDensity (f i) (d i)) (hdisj : (↑s).PairwiseDisjoint f) :
HasDirichletDensity (⋃ i ∈ s, f i) (∑ i ∈ s, d i)

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

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

Dirichlet density is additive on disjoint unions of prime sets.

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

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

source
theorem NumberField.Set.IsLowerDirichletDensityBound.mono_set {K : Type u_1} [Field K] [NumberField K] {S T : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ : ℝ} (hST : S ⊆ T) (hS : IsLowerDirichletDensityBound S δ) :
IsLowerDirichletDensityBound T δ

Lower Dirichlet-density bounds pass to supersets.

source
theorem NumberField.Set.IsUpperDirichletDensityBound.mono_set {K : Type u_1} [Field K] [NumberField K] {S T : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ : ℝ} (hST : S ⊆ T) (hT : IsUpperDirichletDensityBound T δ) :
IsUpperDirichletDensityBound S δ

Upper Dirichlet-density bounds pass to subsets.

source
theorem NumberField.Set.hasDirichletDensity_of_subset_of_subset {K : Type u_1} [Field K] [NumberField K] {S T U : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ : ℝ} (hST : S ⊆ T) (hTU : T ⊆ U) (hS : HasDirichletDensity S δ) (hU : HasDirichletDensity U δ) :
HasDirichletDensity T δ

Squeeze. A set of primes lying between two sets of Dirichlet density δ has Dirichlet density δ.

source
theorem NumberField.Set.isUpperDirichletDensityBound_of_forall_isLowerDirichletDensityBound {K : Type u_1} [Field K] [NumberField K] {δ : ℝ} {ι : Type u_2} {s : Finset ι} {f : ι → Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {d : ι → ℝ} {i₀ : ι} (hi₀ : i₀ ∈ s) (hdisj : (↑s).PairwiseDisjoint f) (hU : IsUpperDirichletDensityBound (⋃ i ∈ s, f i) δ) (hlow : ∀ i ∈ s, i ≠ i₀ → IsLowerDirichletDensityBound (f i) (d i)) (hsum : ∑ i ∈ s, d i = δ) :
IsUpperDirichletDensityBound (f i₀) (d i₀)

Lower bounds on the other members bound this one from above. A finite pairwise disjoint family splits the union's ratio exactly, so one member's ratio is what the others leave behind; if the lower bounds d already sum to δ, and δ bounds the union from above, what they leave behind is d i₀.

Only an upper bound on the union is needed, which is what the proof consumes; a caller holding the full density passes .isUpperDirichletDensityBound.

source
theorem NumberField.Set.hasDirichletDensity_of_squeeze {K : Type u_1} [Field K] [NumberField K] {δ : ℝ} {ι : Type u_2} {s : Finset ι} {f : ι → Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {d : ι → ℝ} {i₀ : ι} (hi₀ : i₀ ∈ s) (hdisj : (↑s).PairwiseDisjoint f) (hU : IsUpperDirichletDensityBound (⋃ i ∈ s, f i) δ) (hlow : ∀ i ∈ s, IsLowerDirichletDensityBound (f i) (d i)) (hsum : ∑ i ∈ s, d i = δ) :
HasDirichletDensity (f i₀) (d i₀)

A lower bound on every member of a finite disjoint family is exact once the bounds saturate the union's upper bound.

Distinct from hasDirichletDensity_of_subset_of_subset, which squeezes a single set between two sets of the same density. Here nothing is sandwiched: the upper bound on one member is manufactured from the other members' lower bounds, because the total is pinned. This is how a one-sided estimate becomes a density — an argument that exhibits enough primes in each class, and cannot see that there are no more, still determines every class exactly.