The all-prime Dirichlet sum is log (1 / (s - 1)) + O(1)

For a number field K, write P(s) = ∑_𝔭 N(𝔭) ^ (-s) for the sum over all height-one primes of 𝓞 K, which is NumberField.Set.primeIdealZetaSum Set.univ s. This file proves that P(s) = log (1 / (s - 1)) + O(1) as s → 1⁺, and hence that Mathlib's ratio-normalized NumberField.Set.HasDirichletDensity agrees with the logarithmically normalized density.

The proof has two inputs, and neither suffices alone.

• The Euler product. For real s > 1, log ζ_K(s) is the convergent sum ∑_𝔭 -log (1 - N(𝔭) ^ (-s)), by TauCeti.log_dedekindZeta_re_eq_tsum_neg_log_one_sub. The higher-prime-power tail theorem TauCeti.abs_tsum_neg_log_one_sub_sub_primeIdealZetaSum_le bounds the difference from P(s) by 2 [K : ℚ], uniformly for s > 1.
• The residue. Mathlib's class number formula NumberField.tendsto_sub_one_mul_dedekindZeta_nhdsGT says that (s - 1) ζ_K(s) tends to the positive residue as s → 1⁺, so log ζ_K(s) - log (1 / (s - 1)) tends to its logarithm.

Main results

• TauCeti.primeIdealZetaSum_univ_le_log_dedekindZeta_re and TauCeti.log_dedekindZeta_re_le_primeIdealZetaSum_univ_add: the two-sided comparison of log ζ_K(s) with P(s), with error at most 2 [K : ℚ].
• TauCeti.tendsto_log_dedekindZeta_re_sub_log_one_div_sub_one: log ζ_K(s) - log (1 / (s - 1)) tends to the logarithm of the residue.
• TauCeti.primeIdealZetaSum_univ_sub_log_one_div_sub_one_isBigO: P(s) - log (1 / (s - 1)) = O(1) as s → 1⁺.
• TauCeti.tendsto_primeIdealZetaSum_univ_atTop: P(s) → ∞ as s → 1⁺.
• TauCeti.tendsto_primeIdealZetaSum_univ_div_log_one_div_sub_one: P(s) / log (1 / (s - 1)) → 1 as s → 1⁺.
• NumberField.Set.hasDirichletDensity_iff_tendsto_div_log_one_div_sub_one: a set of primes has Dirichlet density δ exactly when P_S(s) / log (1 / (s - 1)) → δ.
• NumberField.Set.ofReal_primeIdealZetaSum: P_S(t), cast to ℂ, is the complex sum over all primes of the indicator of S against N(𝔭) ^ (-t).

References

• J. Neukirch, Algebraic Number Theory, Chapter VII, §13.
• J.-P. Serre, A Course in Arithmetic, Chapter VI, §4.1.
• The same argument (Sharifi, Algebraic Number Theory, 7.1.12) is formalized in the Birkbeck–Brasca Chebotarev density project, https://github.com/CBirkbeck/chebotarev-density (Apache-2.0), commit 8575c9df1ae0a61120ab5c964c7911414254bec7, file CebotarevDensity/Density.lean: primeIdealZetaSum_univ_tendsto_log and primeIdealZetaSum_univ_tendsto_atTop, closed there by the helpers of CebotarevDensity/ForMathlib/LogOneDivSubOne.lean that Real.tendsto_log_one_div_sub_atTop and TauCeti.tendsto_div_nhds_one_of_le_add_const_of_sub_const_le adapt. This file follows its outline (Euler-product logarithm, bounded higher-prime-power contribution, simple pole), over HeightOneSpectrum rather than the nonzero prime ideals of 𝓞 K. It derives the logarithmic form of the Euler product from TauCeti.MultiplicativeIdealWeight.exp_tsum_neg_log_one_sub_eq_LSeries and uses the explicit higher-prime-power bound from TauCeti.abs_tsum_neg_log_one_sub_sub_primeIdealZetaSum_le.

theorem TauCeti.primeIdealZetaSum_univ_le_log_dedekindZeta_re {K : Type u_1} [Field K] [NumberField K] {s : ℝ} (hs : 1 < s) : NumberField.Set.primeIdealZetaSum Set.univ s ≤ Real.log (NumberField.dedekindZeta K ↑s).re

The prime sum is at most log ζ_K(s). For real s > 1, the sum of N(𝔭) ^ (-s) over all height-one primes is at most the real logarithm of ζ_K(s).

theorem TauCeti.log_dedekindZeta_re_le_primeIdealZetaSum_univ_add {K : Type u_1} [Field K] [NumberField K] {s : ℝ} (hs : 1 < s) : Real.log (NumberField.dedekindZeta K ↑s).re ≤ NumberField.Set.primeIdealZetaSum Set.univ s + 2 * ↑(Module.finrank ℚ K)

log ζ_K(s) exceeds the prime sum by at most 2 [K : ℚ]. For real s > 1, the real logarithm of ζ_K(s) is at most the all-prime sum at s plus 2 [K : ℚ], a constant independent of s that bounds the contribution of the higher prime powers.

The residue and the logarithmic normalization

theorem TauCeti.tendsto_log_dedekindZeta_re_sub_log_one_div_sub_one {K : Type u_1} [Field K] [NumberField K] : Filter.Tendsto (fun (s : ℝ) => Real.log (NumberField.dedekindZeta K ↑s).re - Real.log (1 / (s - 1))) (nhdsWithin 1 (Set.Ioi 1)) (nhds (Real.log (NumberField.dedekindZeta_residue K)))

log ζ_K(s) = log (1 / (s - 1)) + log κ_K + o(1). As s → 1⁺, the difference between the real logarithm of ζ_K(s) and log (1 / (s - 1)) tends to the logarithm of the residue NumberField.dedekindZeta_residue K. This is the logarithm of Mathlib's class number formula NumberField.tendsto_sub_one_mul_dedekindZeta_nhdsGT.

theorem TauCeti.primeIdealZetaSum_univ_sub_log_one_div_sub_one_isBigO {K : Type u_1} [Field K] [NumberField K] : (fun (s : ℝ) => NumberField.Set.primeIdealZetaSum Set.univ s - Real.log (1 / (s - 1))) =O[nhdsWithin 1 (Set.Ioi 1)] fun (x : ℝ) => 1

The all-prime normalization. As s → 1⁺, the sum of N(𝔭) ^ (-s) over all height-one primes of 𝓞 K is log (1 / (s - 1)) + O(1).

theorem TauCeti.tendsto_primeIdealZetaSum_univ_atTop {K : Type u_1} [Field K] [NumberField K] : Filter.Tendsto (fun (s : ℝ) => NumberField.Set.primeIdealZetaSum Set.univ s) (nhdsWithin 1 (Set.Ioi 1)) Filter.atTop

The all-prime sum diverges at 1. The sum of N(𝔭) ^ (-s) over all height-one primes of 𝓞 K tends to +∞ as s → 1⁺.

theorem TauCeti.tendsto_primeIdealZetaSum_univ_div_log_one_div_sub_one {K : Type u_1} [Field K] [NumberField K] : Filter.Tendsto (fun (s : ℝ) => NumberField.Set.primeIdealZetaSum Set.univ s / Real.log (1 / (s - 1))) (nhdsWithin 1 (Set.Ioi 1)) (nhds 1)

The all-prime sum is asymptotic to log (1 / (s - 1)). The ratio of the sum of N(𝔭) ^ (-s) over all height-one primes of 𝓞 K to log (1 / (s - 1)) tends to 1 as s → 1⁺.

theorem NumberField.Set.hasDirichletDensity_iff_tendsto_div_log_one_div_sub_one {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) (δ : ℝ) : HasDirichletDensity S δ ↔ Filter.Tendsto (fun (s : ℝ) => primeIdealZetaSum S s / Real.log (1 / (s - 1))) (nhdsWithin 1 (Set.Ioi 1)) (nhds δ)

Dirichlet density in logarithmic normalization. A set S of height-one primes of 𝓞 K has Dirichlet density δ, defined as the limit of P_S(s) / P(s) with P the all-prime sum, exactly when P_S(s) / log (1 / (s - 1)) tends to δ as s → 1⁺.

theorem NumberField.Set.ofReal_primeIdealZetaSum {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) (t : ℝ) : ↑(primeIdealZetaSum S t) = ∑' (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)), (if P ∈ S then 1 else 0) / ↑(Ideal.absNorm P.asIdeal) ^ ↑t

The prime-ideal zeta sum as a complex indicator sum. For real t, the sum P_S(t) of N(𝔭) ^ (-t) over S, cast to ℂ, is the sum over all height-one primes of the indicator of S divided by N(𝔭) ^ t.