Frobenius von Mangoldt coefficients

For a conjugacy class C in the Galois group of a finite Galois extension L / K, this file defines the von Mangoldt coefficient and summatory functions restricted to C. A prime power 𝔭 ^ j belongs to the C-fibre when the j-th power of the Artin class of 𝔭 is C. Consequently a prime whose Artin class is not C can still contribute through a higher power.

The definitions retain only unramified primes: the Artin symbol is never evaluated at a ramified prime. The exponent-one terms form frobeniusTheta; all higher prime powers are dominated by the unrestricted higher-prime-power weight from the arithmetic Dirichlet-series development, hence their contribution is o(x).

Main definitions

• NumberField.Chebotarev.frobeniusPrimePowerSet: prime powers selected by the powered Artin class.
• NumberField.Chebotarev.frobeniusVonMangoldtCoeff: the corresponding nonnegative arithmetic function, regrouped by absolute norm.
• NumberField.Chebotarev.frobeniusPsi and NumberField.Chebotarev.frobeniusTheta: the weighted prime-power and prime summatory functions.
• NumberField.Chebotarev.frobeniusPrimeCount: the number of primes of norm at most x whose arithmetic Frobenius class is C, with NumberField.Chebotarev.natCast_frobeniusPrimeCount identifying it with the generic count of frobeniusPrimeSet.

Main results

• NumberField.Chebotarev.frobeniusVonMangoldtCoeff_rat_natGenerator_pow: over ℚ, the coefficient at p ^ (k + 1) is the powered Frobenius weight of 𝔭 ^ (k + 1), the only ideal of that norm.
• NumberField.Chebotarev.frobeniusPsi_eq_sum_range: frobeniusPsi is the inclusive partial sum of frobeniusVonMangoldtCoeff.
• NumberField.Chebotarev.frobeniusPsi_eq_sum_Icc: the same sum indexed from 1.
• NumberField.Chebotarev.frobeniusPsi_sub_frobeniusTheta_eq_primePowerSummatory: their difference is exactly the contribution from exponents at least two.
• NumberField.Chebotarev.frobeniusPsi_sub_frobeniusTheta_le: that difference is bounded by the unrestricted higher-prime-power tail.
• NumberField.Chebotarev.frobeniusPsi_sub_frobeniusTheta_isLittleO: this difference is o(x).

The coefficient convention follows Neukirch, Algebraic Number Theory, Chapter VII. The construction reuses Tau Ceti's generic prime-power counting and removal estimates.

def NumberField.Chebotarev.frobeniusPrimePowerSet (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 (TauCeti.IdealPrimePower K)

The prime powers whose powered Artin class is C. A prime power 𝔭 ^ j is included when 𝔭 is unramified in L and (artinSymbol 𝔭) ^ j = C.

@[simp]

theorem NumberField.Chebotarev.mem_frobeniusPrimePowerSet_iff {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] {A : TauCeti.IdealPrimePower K} {C : ConjClasses Gal(L/K)} : A ∈ frobeniusPrimePowerSet K L C ↔ ∃ (hur : ∀ (Q : Ideal (RingOfIntegers L)) [inst : Q.IsPrime] [Q.LiesOver (TauCeti.primePowerBase A).asIdeal], Algebra.IsUnramifiedAt (RingOfIntegers K) Q), artinSymbol (TauCeti.primePowerBase A).asIdeal hur ^ TauCeti.primePowerExponent A = C

Membership in frobeniusPrimePowerSet, unfolded.

theorem NumberField.Chebotarev.mem_frobeniusPrimePowerSet_iff_artinSymbol_pow_eq {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] {A : TauCeti.IdealPrimePower K} (hur : ∀ (Q : Ideal (RingOfIntegers L)) [inst : Q.IsPrime] [Q.LiesOver (TauCeti.primePowerBase A).asIdeal], Algebra.IsUnramifiedAt (RingOfIntegers K) Q) (C : ConjClasses Gal(L/K)) : A ∈ frobeniusPrimePowerSet K L C ↔ artinSymbol (TauCeti.primePowerBase A).asIdeal hur ^ TauCeti.primePowerExponent A = C

With an unramifiedness proof fixed, membership in the powered Frobenius fibre is the stated equality of conjugacy classes. In particular, membership is independent of that proof.

theorem NumberField.Chebotarev.ofPrime_mem_frobeniusPrimePowerSet_iff {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] {𝔭 : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)} {C : ConjClasses Gal(L/K)} : TauCeti.IdealPrimePower.ofPrime 𝔭 ∈ frobeniusPrimePowerSet K L C ↔ 𝔭 ∈ frobeniusPrimeSet K L C

At exponent one, the powered Frobenius fibre is the ordinary Frobenius prime set.

noncomputable def NumberField.Chebotarev.frobeniusPrimePowerWeight (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)) (A : TauCeti.IdealPrimePower K) : ℝ

The logarithmic weight on prime powers selected by their powered Artin class.

@[simp]

theorem NumberField.Chebotarev.frobeniusPrimePowerWeight_of_mem {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)} {A : TauCeti.IdealPrimePower K} (hA : A ∈ frobeniusPrimePowerSet K L C) : frobeniusPrimePowerWeight K L C A = TauCeti.primePowerWeight A

A prime power in the C-fibre has weight log N(𝔭).

theorem NumberField.Chebotarev.frobeniusPrimePowerWeight_of_artinSymbol_pow_eq {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] {A : TauCeti.IdealPrimePower K} (hur : ∀ (Q : Ideal (RingOfIntegers L)) [inst : Q.IsPrime] [Q.LiesOver (TauCeti.primePowerBase A).asIdeal], Algebra.IsUnramifiedAt (RingOfIntegers K) Q) {C : ConjClasses Gal(L/K)} (hC : artinSymbol (TauCeti.primePowerBase A).asIdeal hur ^ TauCeti.primePowerExponent A = C) : frobeniusPrimePowerWeight K L C A = TauCeti.primePowerWeight A

A prime power whose powered Artin class is C contributes its full logarithmic weight. This exposes the power in the filter: the unpowered Artin class need not equal C.

@[simp]

theorem NumberField.Chebotarev.frobeniusPrimePowerWeight_of_notMem {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)} {A : TauCeti.IdealPrimePower K} (hA : A ∉ frobeniusPrimePowerSet K L C) : frobeniusPrimePowerWeight K L C A = 0

A prime power outside the C-fibre has weight zero.

theorem NumberField.Chebotarev.frobeniusPrimePowerWeight_nonneg {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)) (A : TauCeti.IdealPrimePower K) : 0 ≤ frobeniusPrimePowerWeight K L C A

The powered Frobenius von Mangoldt weight is nonnegative.

theorem NumberField.Chebotarev.frobeniusPrimePowerWeight_le {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)) (A : TauCeti.IdealPrimePower K) : frobeniusPrimePowerWeight K L C A ≤ TauCeti.primePowerWeight A

The powered Frobenius weight is bounded by the unrestricted von Mangoldt weight.

@[simp]

theorem NumberField.Chebotarev.frobeniusPrimePowerWeight_ofPrime {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)) (𝔭 : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) : frobeniusPrimePowerWeight K L C (TauCeti.IdealPrimePower.ofPrime 𝔭) = (frobeniusPrimeSet K L C).indicator (fun (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) => Real.log ↑(Ideal.absNorm v.asIdeal)) 𝔭

On a prime, the powered Frobenius weight is the usual logarithmic indicator of the unpowered Frobenius prime set.

noncomputable def NumberField.Chebotarev.frobeniusPsi (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)) (x : ℝ) : ℝ

Chebyshev's ψ restricted by powered Frobenius class: the inclusive sum of log N(𝔭) over 𝔭 ^ j of norm at most x for which (artinSymbol 𝔭) ^ j = C.

noncomputable def NumberField.Chebotarev.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)) (x : ℝ) : ℝ

Chebyshev's ϑ restricted to the primes whose unpowered Artin class is C.

noncomputable def NumberField.Chebotarev.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)) (x : ℝ) : ℕ

The number of primes of K of norm at most x whose arithmetic Frobenius in L/K belongs to C. Only primes unramified in L are counted.

theorem NumberField.Chebotarev.frobeniusPrimeCount_eq_card {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)) (x : ℝ) : frobeniusPrimeCount K L C x = Nat.card { 𝔭 : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K) // 𝔭 ∈ frobeniusPrimeSet K L C ∧ ↑(Ideal.absNorm 𝔭.asIdeal) ≤ x }

The Frobenius prime count is the cardinality of the primes in the class below the cutoff.

theorem NumberField.Chebotarev.frobeniusPsi_apply {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)) (x : ℝ) : frobeniusPsi K L C x = ∑ A ∈ TauCeti.primePowersLE K x, frobeniusPrimePowerWeight K L C A

frobeniusPsi as an explicit sum over the inclusive prime-power carrier.

theorem NumberField.Chebotarev.frobeniusTheta_apply {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)) (x : ℝ) : frobeniusTheta K L C x = ∑ 𝔭 ∈ TauCeti.primesLE K x, (frobeniusPrimeSet K L C).indicator (fun (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) => Real.log ↑(Ideal.absNorm v.asIdeal)) 𝔭

frobeniusTheta as an explicit sum over the inclusive prime carrier.

theorem NumberField.Chebotarev.frobeniusTheta_def {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)) (x : ℝ) : frobeniusTheta K L C x = TauCeti.primeTheta K (frobeniusPrimeSet K L C) x

The Frobenius ϑ function is the generic logarithmically weighted prime count of its Frobenius prime set.

theorem NumberField.Chebotarev.natCast_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)) (x : ℝ) : ↑(frobeniusPrimeCount K L C x) = TauCeti.primeCount K (frobeniusPrimeSet K L C) x

The Frobenius prime count is the generic count of its prime set.

theorem NumberField.Chebotarev.frobeniusPsi_nonneg {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)) (x : ℝ) : 0 ≤ frobeniusPsi K L C x

The Frobenius ψ function is nonnegative.

theorem NumberField.Chebotarev.frobeniusPsi_mono {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)) : Monotone (frobeniusPsi K L C)

The Frobenius ψ function is monotone in its inclusive cutoff.

theorem NumberField.Chebotarev.frobeniusTheta_nonneg {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)) (x : ℝ) : 0 ≤ frobeniusTheta K L C x

The Frobenius ϑ function is nonnegative.

theorem NumberField.Chebotarev.frobeniusTheta_mono {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)) : Monotone (frobeniusTheta K L C)

The Frobenius ϑ function is monotone in its inclusive cutoff.

noncomputable def NumberField.Chebotarev.frobeniusVonMangoldtWeight (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)) (I : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) : ℝ

The powered Frobenius weight on nonzero ideals, extended by zero away from prime powers.

@[simp]

theorem NumberField.Chebotarev.frobeniusVonMangoldtWeight_idealPrimePower {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)) (A : TauCeti.IdealPrimePower K) : frobeniusVonMangoldtWeight K L C ↑A = frobeniusPrimePowerWeight K L C A

On the prime-power carrier, the ideal weight is the powered Frobenius weight.

@[simp]

theorem NumberField.Chebotarev.frobeniusVonMangoldtWeight_eq_zero_of_not_isPrimePow {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)) {I : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))} (hI : ¬IsPrimePow ↑I) : frobeniusVonMangoldtWeight K L C I = 0

The ideal weight vanishes away from prime-power ideals.

theorem NumberField.Chebotarev.frobeniusVonMangoldtWeight_nonneg {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)) (I : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) : 0 ≤ frobeniusVonMangoldtWeight K L C I

The ideal weight is nonnegative.

noncomputable def NumberField.Chebotarev.frobeniusVonMangoldtCoeff (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)) : ArithmeticFunction ℝ

The Frobenius von Mangoldt coefficient at n: the sum of log N(𝔭) over prime powers 𝔭 ^ j of absolute norm n whose j-th powered Artin class is C.

theorem NumberField.Chebotarev.frobeniusVonMangoldtCoeff_apply {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)) (n : ℕ) : (frobeniusVonMangoldtCoeff K L C) n = ∑ I ∈ TauCeti.normFiber K n, frobeniusVonMangoldtWeight K L C I

The Frobenius von Mangoldt coefficient is the sum of its ideal weights over the norm fibre.

theorem NumberField.Chebotarev.frobeniusVonMangoldtCoeff_nonneg {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)) (n : ℕ) : 0 ≤ (frobeniusVonMangoldtCoeff K L C) n

Frobenius von Mangoldt coefficients are nonnegative.

theorem NumberField.Chebotarev.frobeniusVonMangoldtCoeff_eq_zero_of_not_isPrimePow {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)) {n : ℕ} (hn : ¬IsPrimePow n) : (frobeniusVonMangoldtCoeff K L C) n = 0

The Frobenius von Mangoldt coefficient vanishes unless its index is a prime power.

@[simp]

theorem NumberField.Chebotarev.frobeniusVonMangoldtCoeff_apply_one {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)) : (frobeniusVonMangoldtCoeff K L C) 1 = 0

The Frobenius von Mangoldt coefficient vanishes at 1.

@[simp]

theorem NumberField.Chebotarev.frobeniusVonMangoldtCoeff_rat_natGenerator_pow {L : Type u_3} [Field L] [NumberField L] [IsGalois ℚ L] (C : ConjClasses Gal(L/ℚ)) (𝔭 : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers ℚ)) (k : ℕ) : (frobeniusVonMangoldtCoeff ℚ L C) (Rat.HeightOneSpectrum.natGenerator 𝔭 ^ (k + 1)) = frobeniusPrimePowerWeight ℚ L C (𝔭.idealPrimePowerOf k)

Over ℚ, the Frobenius von Mangoldt coefficient at p ^ (k + 1), for p the rational prime below 𝔭, is the powered Frobenius weight of 𝔭 ^ (k + 1), the only ideal of that norm.

theorem NumberField.Chebotarev.frobeniusPsi_eq_sum_range {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)) (x : ℝ) : frobeniusPsi K L C x = ∑ n ∈ Finset.range (⌊x⌋₊ + 1), (frobeniusVonMangoldtCoeff K L C) n

Frobenius ψ is the inclusive partial sum of the Frobenius von Mangoldt coefficients.

theorem NumberField.Chebotarev.frobeniusPsi_eq_sum_Icc {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)) (x : ℝ) : frobeniusPsi K L C x = ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, (frobeniusVonMangoldtCoeff K L C) n

Frobenius ψ is the sum of its von Mangoldt coefficients indexed from 1.

theorem NumberField.Chebotarev.frobeniusPsi_sub_frobeniusTheta_eq_primePowerSummatory {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)) (x : ℝ) : frobeniusPsi K L C x - frobeniusTheta K L C x = TauCeti.primePowerSummatory K ((frobeniusPrimePowerSet K L C).indicator TauCeti.higherPrimePowerWeight) x

The gap between the Frobenius ψ and ϑ functions is exactly the sum of the higher prime-power weight over the C-fibre.

theorem NumberField.Chebotarev.frobeniusTheta_le_frobeniusPsi {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)) (x : ℝ) : frobeniusTheta K L C x ≤ frobeniusPsi K L C x

The higher prime powers make a nonnegative contribution to Frobenius ψ.

theorem NumberField.Chebotarev.frobeniusPsi_sub_frobeniusTheta_le {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)) (x : ℝ) : frobeniusPsi K L C x - frobeniusTheta K L C x ≤ TauCeti.primePsi K Set.univ x - TauCeti.primeTheta K Set.univ x

The Frobenius higher-prime-power tail is bounded by the unrestricted one. The gap between Frobenius ψ and ϑ is at most the corresponding gap for all primes.

theorem NumberField.Chebotarev.frobeniusPsi_sub_frobeniusTheta_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)) : (fun (x : ℝ) => frobeniusPsi K L C x - frobeniusTheta K L C x) =o[Filter.atTop] fun (x : ℝ) => x

The higher-prime-power contribution to Frobenius ψ is o(x).