Prime counting and natural density for Frobenius classes

For a finite Galois extension L/K of number fields, the primes of K in a conjugacy class C, counted by NumberField.Chebotarev.frobeniusPrimeCount, have count asymptotic to (#C / #Gal(L/K)) Li(x). The weighted Chebotarev theorem gives the corresponding result for ψ_C; removing higher prime powers and Abel summation give the count. The count for the trivial extension gives the all-prime denominator, and comparison with it then gives natural density.

Main results

• NumberField.Chebotarev.tendsto_frobeniusTheta: the weighted prime count divided by x tends to #C / #Gal(L/K).
• NumberField.Chebotarev.tendsto_frobeniusPrimeCount: the prime count divided by x / log x tends to #C / #Gal(L/K).
• NumberField.Chebotarev.frobeniusPrimeCount_isEquivalent_logIntegral: the prime count is asymptotic to (#C / #Gal(L/K)) Li(x).
• NumberField.Chebotarev.hasNaturalDensity_frobeniusPrimeSet: the same ratio is the natural density of the Frobenius prime set.

References

• J. Neukirch, Algebraic Number Theory, Chapter VII, §13.
• S. Lang, Algebraic Number Theory, Chapter XV, for the passage from ψ to prime counting.

theorem NumberField.Chebotarev.tendsto_frobeniusTheta (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (C : ConjClasses Gal(L/K)) : Filter.Tendsto (fun (x : ℝ) => frobeniusTheta K L C x / x) Filter.atTop (nhds (↑(Nat.card ↑C.carrier) / ↑(Nat.card Gal(L/K))))

The Frobenius ϑ function divided by x tends to #C / #Gal(L/K).

theorem NumberField.Chebotarev.frobeniusPrimeCount_isEquivalent_logIntegral (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (C : ConjClasses Gal(L/K)) : Asymptotics.IsEquivalent Filter.atTop (fun (x : ℝ) => ↑(frobeniusPrimeCount K L C x)) fun (x : ℝ) => ↑(Nat.card ↑C.carrier) / ↑(Nat.card Gal(L/K)) * TauCeti.Real.logIntegral x

The Frobenius prime count is asymptotic to (#C / #Gal(L/K)) Li(x).

theorem NumberField.Chebotarev.tendsto_frobeniusPrimeCount (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (C : ConjClasses Gal(L/K)) : Filter.Tendsto (fun (x : ℝ) => ↑(frobeniusPrimeCount K L C x) / (x / Real.log x)) Filter.atTop (nhds (↑(Nat.card ↑C.carrier) / ↑(Nat.card Gal(L/K))))

Qualitative prime-counting Chebotarev: the proportion relative to x / log x of primes whose arithmetic Frobenius lies in C tends to #C / #Gal(L/K).

theorem NumberField.Chebotarev.hasNaturalDensity_frobeniusPrimeSet (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (C : ConjClasses Gal(L/K)) : Set.HasNaturalDensity (frobeniusPrimeSet K L C) (↑(Nat.card ↑C.carrier) / ↑(Nat.card Gal(L/K)))

Natural-density Chebotarev: among the primes of K, the primes with arithmetic Frobenius class C have density #C / #Gal(L/K).