Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Coprime Prime Sum

Abstract

Coprime Prime Sum.

Theorem 1.1 (Coprime Prime Sum).

Lean statement: D5/S3/Analytic/Zeta/NumberField/CoprimePrimeSum.primeIdealZetaSum_unramified_coprime_div_log_tendsto_one

Proof. Machine-checked in Lean as D5/S3/Analytic/Zeta/NumberField/CoprimePrimeSum.primeIdealZetaSum_unramified_coprime_div_log_tendsto_one (✓ std3). ∎

Citation. Chris Birkbeck and the Chebotarev density contributors (2026). Chebotarev density in Lean. URL: https://github.com/CBirkbeck/chebotarev-density/tree/a00054a0e6bbc394b0e81de750db0cd2efc8bd88.

Commentary.

The coprime-norm-unramified prime sum is asymptotic to log(1/(s-1)): it differs from the universal prime sum (primeIdealZetaSum_univ_tendsto_log) by the finitely many excluded primes — ramified or with norm not coprime to m — whose bounded contribution is negligible against log → ∞.

References