Dirichlet density of a set of prime ideals #

Let K be a number field. Given a set S of nonzero prime ideals of 𝓞 K, its Dirichlet density is $$ \delta(S) = \lim_{s \to 1^+} \frac{\sum_{\mathfrak p \in S} \operatorname{N} \mathfrak p^{-s}} {\sum_{\mathfrak p} \operatorname{N} \mathfrak p^{-s}}, $$ when this limit exists. The sum in the denominator runs over all nonzero prime ideals of 𝓞 K.

This is captured by the predicate HasDirichletDensity S δ, stating that the ratio tends to δ, and by the definition dirichletDensity S, the density as a real number (with junk value 0 when it does not exist).

Main results #

NumberField.primeIdealZetaSum_le_card_of_finite — for a finite S, the partial sum is bounded above by the number of elements of S.
NumberField.hasDirichletDensity_empty — the empty set has Dirichlet density 0.
NumberField.dirichletDensity_nonneg — the Dirichlet density is nonnegative.
NumberField.dirichletDensity_le_one — the Dirichlet density is at most 1.

source

noncomputable def NumberField.Set.primeIdealZetaSum {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) (s : ℝ) :

ℝ

The partial Dirichlet series $\sum_{\mathfrak p \in S} \operatorname{N} \mathfrak p^{-s}$.

Equations

NumberField.Set.primeIdealZetaSum S s = ∑' (𝔭 : ↑S), ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s)

Instances For

source

theorem NumberField.Set.primeIdealZetaSum_def {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) (s : ℝ) :

primeIdealZetaSum S s = ∑' (𝔭 : ↑S), ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s)

source

theorem NumberField.Set.primeIdealZetaSum_nonneg {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) (s : ℝ) :

0 ≤ primeIdealZetaSum S s

source

theorem NumberField.Set.primeIdealZetaSum_le_card_of_finite {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} (hS : S.Finite) {s : ℝ} (hs : 0 ≤ s) :

primeIdealZetaSum S s ≤ ↑S.ncard

For a finite set S of prime ideals, the partial sum $\sum_{\mathfrak p \in S} \operatorname{N} \mathfrak p^{-s}$ is bounded above by the number of elements of S.

source

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

Prop

S has Dirichlet density δ when the ratio of the partial sum over S to the sum over all nonzero prime ideals, $$ \frac{\sum_{\mathfrak p \in S} \operatorname{N} \mathfrak p^{-s}} {\sum_{\mathfrak p} \operatorname{N} \mathfrak p^{-s}}, $$ tends to δ as $s \to 1^+$.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable def NumberField.Set.dirichletDensity {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) :

ℝ

The Dirichlet density of S as a real number, taking the junk value 0 when S has no density. As with tsum, this value only has content when S has a density; the genuine statement that S has density 0 is HasDirichletDensity S 0.

Equations