Counting carriers for ideals and prime ideals #
Every estimate in the arithmetic-Dirichlet-series roadmap counts objects whose absolute norm does
not exceed a real cutoff x, and always inclusively: an object of norm exactly x is counted.
This file fixes that convention once.
The common core is Mathlib's Northcott property: a function N : ι → ℕ is Northcott when each
set {i | N i ≤ B} is finite. For such an N:
TauCeti.normLE N xis the finite set of indices with(N i : ℝ) ≤ x;TauCeti.summatory N w xis the inclusive sum of a weightwoverTauCeti.normLE N x.
Two instances of this core carry the arithmetic content, TauCeti.idealsLE for the nonzero
integral ideals of 𝓞 K and TauCeti.primesLE for the height-one primes, with
TauCeti.idealSummatory, TauCeti.primeSummatory, and TauCeti.primePowerSummatory the associated
summatory functions. The
weighted prime counts of the roadmap are the two named specializations
TauCeti.primeTheta, the logarithmically weighted count, and TauCeti.primeCount, the
unweighted one; both are restricted to a set S of height-one primes through Set.indicator,
so no decidability hypothesis is needed on S.
A prime-power ideal is 𝔭 ^ k for a unique height-one prime 𝔭 and a unique k ≥ 1;
TauCeti.primePowerBase and TauCeti.primePowerExponent name that pair, and
TauCeti.idealPrimePower_eq_of_base_eq_of_exponent_eq records that it determines the ideal. The
exponent is 1 exactly on the primes themselves, which is TauCeti.primePowerExponent_eq_one_iff;
TauCeti.IdealPrimePower.ofPrime is the resulting inclusion of the prime carrier into the
prime-power carrier, and TauCeti.primePowerSummatory_eq_primeSummatory uses it to read a
prime-power sum concentrated on the exponent-one part as a sum over primes.
TauCeti.idealsLE_filter_dvd identifies the ideals below a cutoff divisible by a fixed nonzero
ideal P with the multiples of P, and TauCeti.idealSummatory_ite_dvd reads the corresponding
part of a summatory function at the rescaled cutoff x / N(P).
Two lemmas move a summatory function between the three carriers.
TauCeti.idealSummatory_eq_primePowerSummatory reads an ideal weight vanishing off the prime
powers as a prime-power weight, and TauCeti.idealSummatory_eq_sum_range_normFiber regroups an
ideal summatory function into the partial sum, over n ≤ ⌊x⌋₊, of the total mass on the norm
fibre at n; TauCeti.idealSummatory_eq_sum_Icc_normCoeff writes the same regrouping as a
partial sum of TauCeti.normCoeff. Together they present a sum over prime powers as a partial
sum of an ArithmeticFunction, which is the shape a Tauberian theorem consumes.
For 0 ≤ x, a real cutoff and its floor select the same indices, so
TauCeti.normLE_eq_normLE_natFloor and TauCeti.summatory_eq_summatory_natFloor convert between
the real and natural conventions. The small-cutoff cases are degenerate for a reason worth
recording: a nonzero ideal has absolute norm at least 1, and a height-one prime at least 2, so
TauCeti.idealsLE_one isolates the unit ideal and TauCeti.primesLE_eq_empty_of_lt_two empties the
prime carrier below 2.
Modifying a weight on a finite set, or a prime set on a finite symmetric difference, changes a
summatory function by a quantity that is eventually the constant total discrepancy; this is
TauCeti.eventually_summatory_sub_eq and its two prime specializations. Layer 7 uses these to
show that finite changes do not affect a density. In the same spirit,
TauCeti.primeTheta_isLittleO_of_finite records that a finite set of primes contributes an
eventually constant amount to ϑ_K, hence o(x): an exceptional set can be discarded from a
counting argument outright, not merely from a density. Its ψ companion is
TauCeti.primePsi_isLittleO_of_finite.
Roadmap role #
This is Layer 4 of TauCetiRoadmap/ArithmeticDirichletSeries/README.md: the finite cutoff
carriers of 4.1, the generic summatory functions on ideals, primes, and prime powers of 4.2, and the
weighted prime counts primeTheta and primeCount of 4.3. Layer 5 supplies the actual size
estimates for these counts, and consumes the prime base and exponent of a prime-power ideal to
fibre those estimates over the primes.
References #
- G. Tenenbaum, Introduction to Analytic and Probabilistic Number Theory, Chapters I--II.
- H. Davenport, Multiplicative Number Theory, Chapters 1 and 7.
- J. Neukirch, Algebraic Number Theory, Chapter VII.
Ideals and height-one primes of bounded absolute norm #
The absolute norm on nonzero ideals of an infinite Dedekind domain with finite quotients is
Northcott, by Ring.HasFiniteQuotients.finite_absNorm_le. Mathlib already supplies the
corresponding instance on height-one primes.
The nonzero integral ideals of 𝓞 K of absolute norm at most x.
Equations
- TauCeti.idealsLE K x = TauCeti.normLE (fun (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) => Ideal.absNorm ↑I) x
Instances For
The height-one primes of 𝓞 K of absolute norm at most x.
Equations
- TauCeti.primesLE K x = TauCeti.normLE (fun (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => Ideal.absNorm v.asIdeal) x
Instances For
A nonzero integral ideal which is a positive power of a prime ideal.
Equations
- TauCeti.IdealPrimePower K = { A : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) // IsPrimePow ↑A }
Instances For
Absolute norm is Northcott on prime-power ideals, by restriction from nonzero ideals.
The prime-power ideals of 𝓞 K of absolute norm at most x.
Equations
- TauCeti.primePowersLE K x = TauCeti.normLE (fun (A : TauCeti.IdealPrimePower K) => Ideal.absNorm ↑↑A) x
Instances For
Prime-power cutoff carriers grow monotonically with the cutoff.
The absolute norm of a nonzero integral ideal is at least 1, as a real number.
The absolute norm of a height-one prime is at least 2, as a real number.
The absolute norm of a prime-power ideal is at least 2, as a real number.
The prime base and the exponent of a prime-power ideal #
The exponent of a prime-power ideal A: the unique k ≥ 1 with A = 𝔭 ^ k.
Equations
Instances For
The prime base of a prime-power ideal A: the unique height-one prime 𝔭 with
A = 𝔭 ^ k for some k ≥ 1.
Equations
- TauCeti.primePowerBase A = { asIdeal := Exists.choose ⋯, isPrime := ⋯, ne_bot := ⋯ }
Instances For
The ideal underlying the prime base of a prime-power ideal is prime.
The exponent of a prime-power ideal is positive.
The defining factorization of a prime-power ideal.
The prime base is determined by any factorization of A as a power of a prime.
The prime base is the only height-one prime dividing a prime-power ideal.
The absolute norm of a prime-power ideal is the corresponding power of the norm of its prime base.
Membership in the prime-power cutoff, read off the base and the exponent. The cutoff
bounds a prime power's own absolute norm, and that norm is N(𝔭) ^ k, so membership is exactly
the bound the counting arguments use. Both steps are equivalences, so this is an iff.
Deliberately not @[simp]: mem_normLE already carries @[simp, grind =] on the same
reducible head and would compete with it.
The absolute norm of a prime-power ideal is a prime power: N(𝔭 ^ k) = p ^ (f k) for the
rational prime p below 𝔭 and the residue degree f.
The exponent is determined by any factorization of A as a power of a prime.
A prime-power ideal is determined by its prime base and its exponent.
A prime-power ideal has exponent one exactly when it is itself prime.
A prime-power ideal which is not prime has exponent at least two.
A height-one prime, seen as the prime-power ideal of exponent one that it is.
Instances For
The ideal underlying TauCeti.IdealPrimePower.ofPrime v is the prime ideal of v.
The underlying ideal of a height-one prime is prime.
A height-one prime is its own prime base.
A height-one prime has exponent one as a prime-power ideal.
A prime prime-power ideal is its own prime base, seen as a prime-power ideal.
Below the cutoff 1 there is no nonzero integral ideal to count.
At the cutoff 1 the only nonzero integral ideal counted is the unit ideal.
The multiples of a nonzero ideal below a cutoff. The nonzero integral ideals of absolute
norm at most x divisible by P are exactly the products P * J, for J a nonzero integral
ideal of absolute norm at most x / N(P).
Below the cutoff 2 there is no height-one prime to count.
Below the cutoff 2 there is no prime-power ideal to count.
Every real cutoff selects the same prime-power ideals as its natural floor.
There are at most as many prime-power ideals as nonzero integral ideals below any cutoff.
Summatory functions over ideals and over primes #
At a uniform lower-bound cutoff, twisting a weight by a function of its N-value multiplies
the summatory function by the value of the twist at that cutoff.
The inclusive summatory function of a weight on the nonzero integral ideals of 𝓞 K.
Equations
- TauCeti.idealSummatory K w x = TauCeti.summatory (fun (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) => Ideal.absNorm ↑I) w x
Instances For
The inclusive summatory function of a weight on the height-one primes of 𝓞 K.
Equations
- TauCeti.primeSummatory K w x = TauCeti.summatory (fun (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => Ideal.absNorm v.asIdeal) w x
Instances For
The inclusive summatory function of a weight on prime-power ideals of 𝓞 K.
Equations
- TauCeti.primePowerSummatory K w x = TauCeti.summatory (fun (A : TauCeti.IdealPrimePower K) => Ideal.absNorm ↑↑A) w x
Instances For
An ideal summatory function is the sum of its weight over the inclusive cutoff carrier.
A prime summatory function is the sum of its weight over the inclusive cutoff carrier.
A prime-power summatory function is the sum of its weight over the inclusive cutoff carrier.
A prime-power weight vanishing off the primes themselves has the same summatory function as
its restriction to the primes. This is what separates the exponent-one part of a sum over prime
powers, such as Chebyshev's ϑ inside ψ.
Prime-power summation distributes over pointwise addition of weights.
Every real cutoff gives the same prime-power summatory value as its natural floor.
A pointwise nonnegative real weight has a nonnegative prime-power summatory function.
A nonnegative real weight has a prime-power summatory function monotone in the cutoff.
Changing a prime-power weight on finitely many ideals produces an eventually constant difference of summatory functions.
Below the cutoff 1 there is nothing to sum over the nonzero ideals.
At the cutoff 1 only the unit ideal contributes.
Restricting an ideal summatory function to the multiples of a nonzero ideal P. Summing a
weight over the nonzero ideals below x divisible by P is summing the weight of P * J over
the nonzero ideals J below x / N(P), because the absolute norm is multiplicative.
Forbidding one more prime in an ideal partial sum. For a completely multiplicative weight
χ and a prime 𝔭 ∉ S, the partial sums of χ over the ideals prime to insert 𝔭 S are those
over the ideals prime to S, minus χ(𝔭) times the same partial sum at the cutoff divided by
N(𝔭): the ideals prime to S and divisible by 𝔭 are 𝔭 times the ideals prime to S.
Regrouping an ideal summatory function by absolute norm. The inclusive sum of a weight over
the nonzero integral ideals of absolute norm at most x is the sum, over the natural numbers
n ≤ ⌊x⌋₊, of the total mass of the weight on the norm fibre at n.
This is the finite form of the Layer 1 regrouping: it reads a summatory function over ideals as a
partial sum of the ArithmeticFunction obtained from the same weight by TauCeti.normCoeff.
An ideal summatory function is a partial sum of norm coefficients. The inclusive sum of
f over the nonzero integral ideals of absolute norm at most x is ∑_{n=1}^{⌊x⌋₊} of the norm
coefficients of f, in the Finset.Icc 1 form of Mathlib's LSeries_eq_mul_integral.
An ideal weight concentrated on the prime powers, read as a prime-power weight. An ideal
weight vanishing off the prime-power ideals has the same summatory function as its restriction to
the prime-power carrier. This is the ideal-level counterpart of
TauCeti.primePowerSummatory_eq_primeSummatory.
The weighted prime counts #
The logarithmically weighted count of the primes of S of absolute norm at most x: the
number-field analogue of Chebyshev's ϑ.
Equations
- TauCeti.primeTheta K S x = TauCeti.primeSummatory K (S.indicator fun (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => Real.log ↑(Ideal.absNorm v.asIdeal)) x
Instances For
The number of primes of S of absolute norm at most x, as a real number: the number-field
analogue of π.
Equations
- TauCeti.primeCount K S x = TauCeti.primeSummatory K (S.indicator 1) x
Instances For
The logarithmically weighted prime count as an explicit sum over the inclusive carrier.
The unweighted prime count as an explicit sum over the inclusive carrier.
The count of S really is the cardinality of the set of primes of S below the cutoff.
The number of all height-one primes of a number field below the inclusive real cutoff tends to infinity.
This count is the normalizing denominator of a density ratio, so its divergence is what makes such a ratio usable: the denominator is eventually positive, and a finite discrepancy between two numerators vanishes in the limit.
The absolute norm of a height-one prime is positive, as a real number.
The logarithm of the absolute norm of a height-one prime is positive.
The logarithm of the absolute norm of a height-one prime is nonnegative.
A fixed prime base contributes at most log x. For a finset F of prime powers all of
base v and of absolute norm at most x, the total weight #F · log N(v) is at most log x:
distinct members of F have distinct exponents, and every exponent is at most
log x / log N(v).
This is the counting core shared by the two weighted estimates over a prime fibre, which differ
only in which prime powers they collect: TauCeti.higherPrimePowerTheta_le_card_primesLE_mul_log
takes the exponents k ≥ 2, TauCeti.primePsi_le_ncard_mul_log all k ≥ 1. Only 1 ≤ x and a
common base are needed.
The logarithmically weighted prime count is nonnegative.
The unweighted prime count is nonnegative.
The logarithmically weighted prime count is monotone in the inclusive cutoff.
The unweighted prime count is monotone in the inclusive cutoff.
Enlarging the prime set can only increase the logarithmically weighted count.
Enlarging the prime set can only increase the unweighted count.
Below the cutoff 2 no prime is counted.
Below the cutoff 2 no prime is counted by the unweighted count.
Every real cutoff gives the same logarithmically weighted prime count as its natural floor.
Every real cutoff gives the same unweighted prime count as its natural floor.
The weighted counts are additive along a disjoint union of prime sets.
The unweighted count is additive along a disjoint union of prime sets.
The logarithmically weighted count of S exceeds that of T by at most the weighted count
of their symmetric difference.
The unweighted count of S exceeds that of T by at most the count of their symmetric
difference.
Chebyshev's trivial comparison: each counted prime contributes at most log x.
A finite set of primes has eventually constant count, namely its cardinality. This is the input to the Layer 7 statement that a finite set of primes has Dirichlet density zero.
Primes counted below the prime-ideal-theorem order carry negligible weight. Chebyshev's
comparison spends one factor of log x per counted prime, so a count of o(x / log x) gives a
weighted sum of o(x).
Stated for an arbitrary prime set, since the argument uses nothing about which primes are counted;
TauCeti.primeTheta_higherDegreePrimes_isLittleO is the residue-degree instance.
A finite set of primes carries a negligible weight, because its contribution to ϑ_K is
eventually constant: past the largest norm in the set every member is already counted, so the
sum stops growing. A constant is o(x).
This is what lets a counting argument discard an exceptional set outright — the ramified primes of an extension, say — rather than only from a density.
If two prime sets have finite symmetric difference, their logarithmically weighted counts differ eventually by the fixed total discrepancy on that symmetric difference.
If two prime sets have finite symmetric difference, their unweighted counts differ eventually by the fixed total discrepancy on that symmetric difference.