Primes in an arithmetic progression have Dirichlet density 1 / φ(m)

For m ≠ 0 and a a unit modulo m, the height-one primes 𝔭 of 𝓞 ℚ whose absolute norm is congruent to a modulo m have Dirichlet density 1 / φ(m), in the ratio-normalized sense of Mathlib's NumberField.Set.HasDirichletDensity.

Over ℚ these primes correspond to the rational primes p ≡ a (mod m), so the result says how the rational primes distribute among the invertible residue classes modulo m: they are equidistributed, each of the φ(m) classes receiving the same share 1 / φ(m) of the primes, measured by Dirichlet density. This is the Dirichlet-density form of Dirichlet's theorem on primes in arithmetic progressions.

Main results

• NumberField.Chebotarev.primeCount_primesCongruent_sub_mul_logIntegral_isLittleO: the prime count in an invertible residue class is φ(m)⁻¹ Li(x) + o(x / log x).
• NumberField.Chebotarev.hasDirichletDensity_primesCongruent: the primes of 𝓞 ℚ of norm congruent to a unit a modulo m have Dirichlet density 1 / φ(m).

References

The analytic input is Mathlib's Mathlib.NumberTheory.LSeries.PrimesInAP, through the von Mangoldt function restricted to a residue class, ArithmeticFunction.vonMangoldt.residueClass, and its boundary results:

• ArithmeticFunction.vonMangoldt.abscissaOfAbsConv_residueClass_le_one: its L-series converges absolutely for re s > 1;
• ArithmeticFunction.vonMangoldt.eqOn_LFunctionResidueClassAux and ArithmeticFunction.vonMangoldt.continuousOn_LFunctionResidueClassAux: that L-series minus φ(m)⁻¹ / (s - 1) extends continuously to re s ≥ 1;
• ArithmeticFunction.vonMangoldt.summable_residueClass_non_primes_div: the prime powers that are not primes contribute an absolutely convergent series at s = 1.

theorem NumberField.Chebotarev.primeCount_primesCongruent_sub_mul_logIntegral_isLittleO (m a : ℕ) [NeZero m] (ha : IsUnit ↑a) : (fun (x : ℝ) => TauCeti.primeCount ℚ {𝔭 : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers ℚ) | Ideal.absNorm 𝔭.asIdeal % m = a % m} x - (↑m.totient)⁻¹ * TauCeti.Real.logIntegral x) =o[Filter.atTop] fun (x : ℝ) => x / Real.log x

The primes of 𝓞 ℚ of norm congruent to an invertible residue a modulo m satisfy π_S = φ(m)⁻¹ Li + o(x / log x).

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

Dirichlet's theorem on primes in arithmetic progressions, with Dirichlet density. For m ≠ 0 and a a unit modulo m, the primes of 𝓞 ℚ whose absolute norm is congruent to a modulo m have Dirichlet density 1 / φ(m).