Weighted Chebotarev for cyclotomic extensions

Let F = K(μ_m) be a cyclotomic extension of a number field K, with group G = Gal(F/K). This file proves the prime-number-theorem form of Chebotarev's theorem for F / K: for every σ ∈ G,

ψ_σ(x) = x / #G + o(x),

where ψ_σ = frobeniusPsi K F (ConjClasses.mk σ) counts the prime powers 𝔭 ^ j of K with 𝔭 unramified in F and Frob(𝔭) ^ j = σ, weighted by log N𝔭.

The proof applies the Wiener--Ikehara theorem TauCeti.LSeries.wienerIkehara to the nonnegative coefficients of ψ_σ. By the character expansion NumberField.Chebotarev.LSeries_frobeniusVonMangoldtCoeff_eq_sum_logDeriv, their Dirichlet series is (1 / #G) ∑_χ χ(σ)⁻¹ (-L_χ'(s) / L_χ(s)) on Re s > 1, where L_χ is the L-series of the Galois character weight of χ. The required boundary behaviour on Re s ≥ 1 comes term by term:

• for χ ≠ 1, the continued series cyclotomicCharacterSeriesC K F χ is holomorphic across Re s = 1 and nonzero on Re s ≥ 1, so -L_χ'/L_χ extends continuously to Re s ≥ 1;
• for χ = 1, L_1 is the Dedekind zeta function of K with the Euler factors at the ramified primes deleted. The function H(s) = (s - 1) L_1(s) continues holomorphically across Re s = 1, takes the value ρ = Res_{s=1} ζ_K · ∏_{𝔭 ramified} (1 - N𝔭⁻¹) ≠ 0 at s = 1, and does not vanish elsewhere on Re s ≥ 1. Hence -L_1'/L_1 - 1/(s - 1) = -H'/H extends continuously to Re s ≥ 1.

So the Frobenius von Mangoldt series of σ minus (1 / #G) / (s - 1) extends continuously to Re s ≥ 1, which is exactly the Wiener--Ikehara hypothesis with residue 1 / #G.

Main results

• NumberField.Chebotarev.frobeniusPsi_asymptotic_of_isCyclotomicExtension: for F = K(μ_m), ψ_σ(x) = x / #Gal(F/K) + o(x).

References

• J. Neukirch, Algebraic Number Theory, Chapter VII, §13.
• S. Lang, Algebraic Number Theory, Chapter XV.
• The regularization (s - 1) L(s), holomorphic near Re s ≥ 1, follows Mathlib's DirichletCharacter.LFunctionTrivChar₁ and DirichletCharacter.continuousOn_neg_logDeriv_LFunctionTrivChar₁ (Mathlib/NumberTheory/LSeries/DirichletContinuation.lean), used there for Dirichlet's theorem on primes in arithmetic progressions.
• The character-sum boundary function follows Mathlib's ArithmeticFunction.vonMangoldt.LFunctionResidueClassAux and its continuity and agreement theorems in Mathlib/NumberTheory/LSeries/PrimesInAP.lean.

theorem NumberField.Chebotarev.frobeniusPsi_asymptotic_of_isCyclotomicExtension (K : Type u_1) (F : Type u_2) [Field K] [NumberField K] [Field F] [NumberField F] [Algebra K F] [IsGalois K F] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} K F] (σ : Gal(F/K)) : (fun (x : ℝ) => frobeniusPsi K F (ConjClasses.mk σ) x - 1 / ↑(Nat.card Gal(F/K)) * x) =o[Filter.atTop] fun (x : ℝ) => x

Weighted Chebotarev for cyclotomic extensions. For F = K(μ_m) and σ ∈ Gal(F/K), the Frobenius ψ function of σ satisfies ψ_σ(x) = x / #Gal(F/K) + o(x).