Convergence of the ideal- and prime-indexed Dirichlet series #
The nonzero integral ideals of π K carry the Dirichlet series β N(I) ^ (-s), whose abscissa
of absolute convergence is exactly 1: that is TauCeti.summable_idealTerm_one_iff, read off
from the two-sided linear ideal counts. Distinct height-one primes are distinct nonzero
integral ideals, so the prime-indexed series β N(π) ^ (-s) is a subfamily of that one, and
converges for every s > 1. Only convergence transfers this way, not the abscissa: divergence
of the all-prime sum at s = 1 is a separate statement, and is not proved here.
NumberField.Set.primeIdealZetaSum S s is that sum restricted to a set S of primes. It is a
tsum, and a tsum takes the junk value 0 on a family that is not summable, so summability
is what separates a statement about the prime Dirichlet sum from a statement about that junk
value. The results below supply it for every s > 1 and every set of primes.
Main results #
TauCeti.summable_absNorm_rpow_ideal_iff: over the nonzero integral ideals ofπ K, the seriesβ N(I) ^ (-s)converges exactly for1 < s. This is the real-variable form ofTauCeti.summable_idealTerm_one_iff.TauCeti.summable_absNorm_rpow_primes_of_one_lt: over the height-one primes ofπ K, the seriesβ N(π) ^ (-s)converges for every1 < s.TauCeti.summable_absNorm_rpow_subtype_of_one_lt: the same over an arbitrary set of height-one primes. This is the familyNumberField.Set.primeIdealZetaSumsums, so it is the form its consumers need.NumberField.Set.primeIdealZetaSum_univ: the prime ideal zeta sum over all height-one primes as a sum over the whole height-one spectrum.NumberField.Set.primeIdealZetaSum_mono_set: the prime ideal zeta sum is monotone under inclusion of sets of primes, given summability over the larger set;NumberField.Set.primeIdealZetaSum_mono_set_of_one_ltis its1 < sspecialization.NumberField.Set.primeIdealZetaSum_pos: a summable sum over a nonempty set of primes is positive;NumberField.Set.primeIdealZetaSum_univ_posapplies this to all primes. The corresponding_of_one_ltlemmas supply summability from1 < s.
Implementation notes #
The prime-indexed statement is obtained by restricting the ideal-indexed one along
π β¦ π.asIdeal, which is injective into (Ideal (π K))β°, rather than by comparing each
N(π) = p ^ f with the rational prime p below it and summing over the rational primes. The
restriction is the shorter route on the full set of primes, and reuses the exact abscissa already
established for the trivial ideal weight. The comparison route is not redundant: on the primes
of residue degree above one it yields the strictly wider half-line s > 1/2, and
TauCeti.summable_absNorm_rpow_higherDegreePrimes takes it for exactly that reason.
References #
- J. Neukirch, Algebraic Number Theory, Chapter VII, Β§13.
- Adapted from the BirkbeckβBrasca Chebotarev density project,
https://github.com/CBirkbeck/chebotarev-density (Apache-2.0), commit
8575c9df1ae0a61120ab5c964c7911414254bec7, fileCebotarevDensity/Density.lean:summable_absNorm_rpow_ideal_ifffromsummable_nonzeroIdeal_absNorm_rpow,summable_absNorm_rpow_subtype_of_one_ltfromsummable_prime_absNorm_rpow, andNumberField.Set.primeIdealZetaSum_mono_setfromprimeIdealZetaSum_le_of_subset.
The ideal-indexed series, as a real Dirichlet series #
The ideal-indexed Dirichlet series converges exactly on s > 1. The real-variable form
of TauCeti.summable_idealTerm_one_iff, stated for the real power N(I) ^ (-s) rather than for
the complex term TauCeti.idealTerm, which is the shape the prime-indexed results below meet.
The prime-indexed series #
The prime-indexed Dirichlet series converges for s > 1. The height-one-prime analogue of
TauCeti.summable_absNorm_rpow_ideal_iff.
Restricted to any set of height-one primes, the prime-indexed Dirichlet series still
converges for s > 1: a subfamily of a summable family is summable.
This is the family NumberField.Set.primeIdealZetaSum sums, so it is the summability its
consumers need in order to denote a genuine sum rather than the tsum junk value.
The prime ideal zeta sum over all height-one primes is the sum over the whole height-one spectrum.
The prime ideal zeta sum is monotone under inclusion of sets of primes. The hypothesis is
summability over the larger set, which is what the proof actually consumes: a sparse set of primes
can be summable well outside the half-line on which the all-prime series converges.
primeIdealZetaSum_mono_set_of_one_lt is the specialization to 1 < s.
Summability is not decoration: tsum returns 0 on a family that is not summable, so an
inequality between two such sums can fail with a positive left-hand side and a vanishing right.
The 1 < s specialization of primeIdealZetaSum_mono_set, where summability over the larger
set is automatic.
A summable prime ideal zeta sum over a nonempty set of primes is positive. Every term is
positive; summability ensures that the sum is genuine rather than the tsum junk value 0.
The 1 < s specialization of primeIdealZetaSum_pos, where summability is automatic.
A summable sum over all primes is positive. This is the denominator of the ratio defining
NumberField.Set.HasDirichletDensity; the ring of integers is not a field, so it has a height-one
prime.
The 1 < s specialization of primeIdealZetaSum_univ_pos, where summability is automatic.