The Frobenius von Mangoldt series as a character sum of logarithmic derivatives #
Let L / K be a finite abelian Galois extension of number fields with group G, and fix
σ ∈ G. For each character χ : G →* ℂˣ let L_χ be the L-series of the Galois character
weight MonoidHom.galoisCharacterWeight χ, whose Euler product omits the primes ramified in L.
This file proves, for Re s > 1,
∑_{𝔭 unramified, m ≥ 1, Frob(𝔭)^m = σ} log N𝔭 · N𝔭^{-ms}
= (1 / #G) ∑_χ χ(σ)⁻¹ · (-L_χ'(s) / L_χ(s)).
The left-hand side is the LSeries of the canonical coefficient
NumberField.Chebotarev.frobeniusVonMangoldtCoeff, so the identity is a theorem about that
coefficient rather than a hypothesis on an arbitrary sequence. It reduces the
Frobenius-restricted von Mangoldt series to the logarithmic derivatives of the one-dimensional
character series, which is the form the Tauberian step of the Chebotarev argument consumes.
The proof is termwise. By
TauCeti.MultiplicativeIdealWeight.logDeriv_LSeries_eq_neg_tsum_vonMangoldtTransform each
-L_χ'/L_χ is the ideal-indexed series of χ(A) Λ(A). At a prime power A = 𝔭 ^ m the
weight is χ(Frob 𝔭) ^ m = χ(Frob(𝔭) ^ m) when 𝔭 is unramified and 0 otherwise, and
character orthogonality
(AlgEquiv.sum_inv_mul_galoisCharacterWeight_pow_apply_of_unramified) collapses the character
sum at A to #G times the indicator of Frob(𝔭) ^ m = σ. That indicator is exactly the powered
filter of frobeniusVonMangoldtWeight, since in an abelian group the class of Frob(𝔭) ^ m is
{σ} precisely when Frob(𝔭) ^ m = σ.
Main results #
NumberField.Chebotarev.sum_inv_mul_vonMangoldtTransform_galoisCharacterWeight_apply: the character sum of the von Mangoldt transforms at one nonzero ideal is#Gtimes the Frobenius von Mangoldt weight ofσthere.NumberField.Chebotarev.LSeriesSummable_frobeniusVonMangoldtCoeff: the Frobenius von Mangoldt series converges absolutely onRe s > 1, for an arbitrary conjugacy class.NumberField.Chebotarev.LSeries_frobeniusVonMangoldtCoeff_eq_sum_logDeriv: the character expansion of the Frobenius von Mangoldt series.
Implementation notes #
The inverse sits on the tag σ, never on the Frobenius argument. Writing χ σ for (χ σ)⁻¹, or
χ (Frob 𝔭)⁻¹ for χ (Frob 𝔭), replaces the fibre of σ by the fibre of σ⁻¹.
The prime-power filter uses the power of the Frobenius, not the Frobenius itself: the term at
𝔭 ^ m is counted when Frob(𝔭) ^ m = σ, even if Frob 𝔭 ≠ σ. This is what
frobeniusVonMangoldtWeight records and what the orthogonality at the m-th power of the weight
produces, so no separate bookkeeping of the higher prime powers is needed here.
References #
- J. Neukirch, Algebraic Number Theory, Chapter VII, §13.
Character orthogonality for the von Mangoldt transforms. For L / K abelian and σ in its
Galois group, summing (χ σ)⁻¹ against the von Mangoldt transform of the Galois character weight
at a nonzero ideal I gives #Gal(L/K) times the Frobenius von Mangoldt weight of σ at I.
At I = 𝔭 ^ m with 𝔭 unramified this is #Gal(L/K) · log N𝔭 when Frob(𝔭) ^ m = σ and 0
otherwise; at a ramified prime power, and away from the prime powers, both sides vanish.
The regrouped coefficients of the Frobenius von Mangoldt ideal weight are the Frobenius von Mangoldt coefficients.
The Frobenius von Mangoldt series converges absolutely on Re s > 1. Its coefficients are
dominated termwise, ideal by ideal, by the von Mangoldt function of K.
The character expansion of the Frobenius von Mangoldt series. For L / K abelian with
group G, σ ∈ G and Re s > 1,
∑ n, Λ_σ(n) n^{-s} = (1 / #G) ∑_χ χ(σ)⁻¹ · (-L_χ'(s) / L_χ(s)),
where Λ_σ is frobeniusVonMangoldtCoeff K L (ConjClasses.mk σ) and L_χ is the L-series of
MonoidHom.galoisCharacterWeight χ, whose Euler product omits the ramified primes.
The inverse sits on the tag σ: with χ σ in its place the left-hand side would be the series of
the fibre of σ⁻¹.