Prime counting and natural density in arithmetic progressions

Natural-density Chebotarev gives density 1 / φ(m) for each arithmetic Frobenius fibre of ℚ(ζₘ). The cyclotomic Frobenius formula identifies the fibre tagged by a with primes whose norm is congruent to a modulo m, up to finitely many primes dividing the level. Thus each invertible arithmetic progression has the same natural density, measured relative to all primes. No restriction on the nonzero level is needed: the possible discrepancy at two for levels congruent to two modulo four is finite.

The corresponding prime-counting statement is that the number of primes in an invertible progression up to x is asymptotic to Li(x) / φ(m), equivalently its quotient by x / log x tends to 1 / φ(m).

In particular, each of the four fibres of ℚ(ζ₅) has natural density 1/4, agreeing with its Dirichlet density. The existing exact fibre dictionary sends arithmetic Frobenius to the norm modulo five, so the tags 2 and 3 are not interchanged.

References

• L. Washington, Introduction to Cyclotomic Fields, Chapter 2, for cyclotomic Frobenius.
• J. Neukirch, Algebraic Number Theory, Chapter VII, §13, for Chebotarev density.

theorem NumberField.Chebotarev.primeCount_primesCongruent_isEquivalent_logIntegral (m a : ℕ) [NeZero m] (ha : IsUnit ↑a) : Asymptotics.IsEquivalent Filter.atTop (fun (x : ℝ) => TauCeti.primeCount ℚ {p : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers ℚ) | Ideal.absNorm p.asIdeal % m = a % m} x) fun (x : ℝ) => 1 / ↑m.totient * TauCeti.Real.logIntegral x

The prime number theorem for arithmetic progressions. At every nonzero level m, the number of primes of 𝒪 ℚ whose norms are congruent to an invertible residue a modulo m is asymptotic to Li(x) / φ(m). This is the logarithmic-integral form of equidistribution among the invertible residue classes.

theorem NumberField.Chebotarev.tendsto_primeCount_primesCongruent (m a : ℕ) [NeZero m] (ha : IsUnit ↑a) : Filter.Tendsto (fun (x : ℝ) => TauCeti.primeCount ℚ {p : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers ℚ) | Ideal.absNorm p.asIdeal % m = a % m} x / (x / Real.log x)) Filter.atTop (nhds (1 / ↑m.totient))

The number of primes in an invertible residue class modulo m, divided by x / log x, tends to 1 / φ(m).

theorem NumberField.Chebotarev.hasNaturalDensity_frobeniusPrimeSet_galEquivZMod_symm (F : Type u_1) [Field F] [NumberField F] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} ℚ F] [IsGalois ℚ F] (a : (ZMod m)ˣ) : Set.HasNaturalDensity (frobeniusPrimeSet ℚ F (ConjClasses.mk ((IsCyclotomicExtension.Rat.galEquivZMod m F).symm a))) (1 / ↑m.totient)

Over ℚ, the cyclotomic Frobenius fibre tagged by a unit modulo m has natural density 1 / φ(m).

theorem NumberField.Chebotarev.hasNaturalDensity_frobeniusPrimeSet_cyclotomic_five (F : Type u_1) [Field F] [NumberField F] [IsCyclotomicExtension {5} ℚ F] [IsGalois ℚ F] (a : (ZMod 5)ˣ) : Set.HasNaturalDensity (frobeniusPrimeSet ℚ F (ConjClasses.mk ((IsCyclotomicExtension.Rat.galEquivZMod 5 F).symm a))) (1 / 4)

Each arithmetic Frobenius fibre of a fifth cyclotomic field has natural density 1/4, the same value as its Dirichlet density.

theorem NumberField.Chebotarev.hasNaturalDensity_primesCongruent (m a : ℕ) [NeZero m] (ha : IsUnit ↑a) : Set.HasNaturalDensity {𝔭 : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers ℚ) | Ideal.absNorm 𝔭.asIdeal % m = a % m} (1 / ↑m.totient)

Natural density of primes in arithmetic progressions. At every nonzero level m, the primes of 𝓞 ℚ whose norms are congruent to an invertible residue a have natural density 1 / φ(m). The congruence is the arithmetic Frobenius tag, without inversion.