Negligible terms in Frobenius prime counting

Weighted crossing arguments bound the error incurred when passing from a Frobenius prime-power sum to a prime sum of residue degree one by three functions. These account for higher prime powers in the chosen Frobenius class and use unrestricted sums to majorize the contributions from primes of absolute residue degree above one and from a finite exceptional set. Each majorant is o(x) for a different reason. This file records that their sum is o(x).

Main result

• NumberField.Chebotarev.frobeniusDiscard_isLittleO: the sum of three majorants for the discard error is negligible compared with x.

theorem NumberField.Chebotarev.frobeniusDiscard_isLittleO {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)) (T : Finset (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) : (fun (x : ℝ) => frobeniusPsi K L C x - frobeniusTheta K L C x + TauCeti.primeTheta K (TauCeti.higherDegreePrimes K) x + TauCeti.primePsi K (↑T) x) =o[Filter.atTop] fun (x : ℝ) => x

The sum of three majorants for the error incurred when a Frobenius prime-power sum is restricted to residue-degree-one primes outside a finite exceptional set is o(x).

The first summand is the higher-prime-power contribution in the Frobenius fibre. The other two are unrestricted weighted sums over all primes of absolute residue degree greater than one and all prime powers based at an exceptional prime.