The prime ideal theorem

The analytic boundary data of the Dedekind zeta function supplies the generic prime-number-theorem transfer with residue one. This gives asymptotics for the three standard counting functions of prime ideals in a number field: Chebyshev's ψ and ϑ, and the unweighted count π.

Main results

• TauCeti.primeIdealTheorem: ψ_K(x) ~ x, ϑ_K(x) ~ x, and π_K(x) ~ Li(x).
• TauCeti.primeCount_univ_isEquivalent_div_log: the classical form π_K(x) ~ x / log x.

References

• J. Neukirch, Algebraic Number Theory, Chapter VII, §5.
• H. Davenport, Multiplicative Number Theory, Chapter 17.

theorem TauCeti.primeIdealTheorem (K : Type u_1) [Field K] [NumberField K] : (Asymptotics.IsEquivalent Filter.atTop (primePsi K Set.univ) fun (x : ℝ) => x) ∧ (Asymptotics.IsEquivalent Filter.atTop (primeTheta K Set.univ) fun (x : ℝ) => x) ∧ Asymptotics.IsEquivalent Filter.atTop (primeCount K Set.univ) Real.logIntegral

The prime ideal theorem. For a number field K, Chebyshev's functions satisfy ψ_K(x) ~ x and ϑ_K(x) ~ x, and the number π_K(x) of prime ideals of norm at most x satisfies π_K(x) ~ Li(x).

theorem TauCeti.primeCount_univ_isEquivalent_div_log (K : Type u_1) [Field K] [NumberField K] : Asymptotics.IsEquivalent Filter.atTop (primeCount K Set.univ) fun (x : ℝ) => x / Real.log x

The prime ideal theorem, in the form π_K(x) ~ x / log x.