Chebyshev's Ο for a set of prime ideals, and the removal of the higher prime powers #
For a set S of height-one primes of the ring of integers of a number field K, Chebyshev's
Ο weights every prime power π ^ k with π β S and k β₯ 1 by log N(π), while Ο weights
only the primes themselves. This file defines Ο, proves that the difference Ο - Ο is exactly
the higher-prime-power sum estimated in
TauCeti/NumberTheory/ArithmeticDirichletSeries/HigherPrimePowers.lean, and spends that estimate
on the transfer of an asymptotic Ο(x) = Ξ΄ x + o(x) to Ο(x) = Ξ΄ x + o(x).
Prime powers with k β₯ 2 are kept visible throughout: Ο is defined with all of them present,
and their removal is a named hypothesis, TauCeti.HasNegligibleHigherPrimePowers, discharged for
the standard logarithmic weight by TauCeti.standardPrimePowerRemoval. A different coefficient
system does not get that hypothesis for free; what it has to supply is the domination bound of
TauCeti.primePowerSummatory_isLittleO_of_le_higherPrimePowerWeight.
Main definitions #
TauCeti.primePowerWeightis the standard logarithmic prime-power weight, the valuelog N(π)atπ ^ kfor everyk β₯ 1. It is the real form of the ideal von Mangoldt function of Layer 2 on the prime powers.TauCeti.primePsiis its inclusive summatory function over the prime powers whose base lies inS: the number-field analogue of Chebyshev'sΟ.TauCeti.HasNegligibleHigherPrimePowers K Ssays thatΟ - Οiso(x).TauCeti.primeVonMangoldtWeightis the same weight spread over all nonzero ideals, zero away from the prime powers with base inS, andTauCeti.primeVonMangoldtCoeffis its regrouping by absolute norm, anArithmeticFunction β.
Main results #
TauCeti.primePowerSummatory_indicator_sub_primeThetasplits the exponent-one part off the standard weight restricted to any set of prime powers containing exactly the primes ofS.TauCeti.primePsi_sub_primeThetaidentifiesΟ - Οwith the higher-prime-power sum.TauCeti.primePsi_le_ncard_mul_log: forx β₯ 1, a finite set of primes contributes at most#S Β· log xtoΟ, withTauCeti.primePsi_isBigO_log_of_finiteandTauCeti.primePsi_isLittleO_of_finiteits asymptotic forms.TauCeti.standardPrimePowerRemovalprovesHasNegligibleHigherPrimePowers K Sfor everyS, from the Layer 5 estimateΟ(x) - Ο(x) = O(βx logΒ² x).TauCeti.primeTheta_asymptotic_of_primePsiandTauCeti.primePsi_asymptotic_of_primeThetatransfer a linear asymptotic across that difference, withTauCeti.primeTheta_isEquivalent_of_primePsithe equivalence form for a nonzero density.TauCeti.primePsi_eq_sum_rangepresentsΟ(x)as the inclusive partial sumβ_{n β€ βxββ} a nof the coefficient system, whose coefficients are nonnegative (TauCeti.primeVonMangoldtCoeff_nonneg) and supported on the prime powers (TauCeti.primeVonMangoldtCoeff_eq_zero_of_not_isPrimePow).TauCeti.normCoeff_vonMangoldtidentifies the coefficient system of the full prime carrier with the Layer 1 regrouping of the Layer 2 ideal von Mangoldt function.
Roadmap role #
This is Layer 10.2 of TauCetiRoadmap/ArithmeticDirichletSeries/README.md: "For the fixed
standard nonnegative logarithmic prime-power weight, use Layer 5 to prove
standardPrimePowerRemoval : HasNegligibleHigherPrimePowers K S and make
primeTheta_asymptotic_of_primePsi consume that named estimate." It also supplies the arithmetic
half of Layer 10.1, "Define primePsi with all prime powers present": the exact nonnegative
von Mangoldt coefficient system and the identity presenting Ο as its partial sum, which is the
shape in which a Tauberian theorem delivers its conclusion. What remains of 10.1 β the analytic
package PrimeBoundaryRemainder, carrying the LSeriesHasSum and boundary-continuity hypotheses,
and the asymptotic primePsi_asymptotic_of_boundary it yields β waits on the WienerβIkehara
theorem of Layer 9.
References #
- H. Davenport, Multiplicative Number Theory, Chapter 7.
- G. Tenenbaum, Introduction to Analytic and Probabilistic Number Theory, Chapter I.2.
- J. Neukirch, Algebraic Number Theory, Chapter VII.
The rational-prime case of Ο, Ο and their difference is Mathlib's
Mathlib/NumberTheory/Chebyshev.lean, whose Chebyshev.theta_le_psi and
Chebyshev.abs_psi_sub_theta_le_sqrt_mul_log are the analogues of
TauCeti.primeTheta_le_primePsi and TauCeti.standardPrimePowerRemoval; nothing is transported
from there, since the estimate consumed here is proved over prime ideals in Layer 5.
The standard logarithmic prime-power weight #
The standard logarithmic prime-power weight: the value log N(π) at the prime power
π ^ k, for every k β₯ 1. Unlike TauCeti.higherPrimePowerWeight it does not vanish on the
primes themselves, so its summatory function is Chebyshev's Ο rather than Ο - Ο.
Equations
Instances For
The standard logarithmic prime-power weight is the real part of the ideal von Mangoldt function of Layer 2, restricted to the prime powers.
The standard logarithmic prime-power weight is positive.
The standard logarithmic prime-power weight is nonnegative.
On a prime the standard weight is the logarithm of its own absolute norm.
Away from the primes the two prime-power weights agree: TauCeti.higherPrimePowerWeight is
the standard weight with its exponent-one part deleted.
Chebyshev's Ο #
Chebyshev's Ο for a set of prime ideals: the inclusive sum of log N(π) over the prime
powers π ^ k of absolute norm at most x whose base π lies in S, with every exponent
k β₯ 1 present.
Equations
Instances For
Chebyshev's Ο as an explicit sum over the inclusive prime-power carrier.
The empty set of primes contributes nothing to Ο.
Chebyshev's Ο is nonnegative.
Chebyshev's Ο is monotone in the inclusive cutoff.
Below the cutoff 2 there is no prime power to weight.
The higher prime powers as the gap between Ο and Ο #
Splitting the exponent-one part off a restricted prime-power sum. For a set T of prime
powers containing exactly the primes of S, the summatory function of the standard logarithmic
weight restricted to T exceeds Ο by the higher-prime-power sum over T.
The difference between Ο and Ο is the higher-prime-power sum. Both sides run over the
prime powers whose base lies in S; the exponent-one part of Ο is exactly Ο.
Chebyshev's Ο never exceeds Ο.
Removing the higher prime powers #
The higher prime powers of S are negligible: Ο - Ο is o(x). Naming the hypothesis
keeps the estimate an input to the prime-number-theorem transfer instead of a definitional
simplification of Ο.
Equations
- TauCeti.HasNegligibleHigherPrimePowers K S = (fun (x : β) => TauCeti.primePsi K S x - TauCeti.primeTheta K S x) =o[Filter.atTop] fun (x : β) => x
Instances For
The defining little-o estimate behind TauCeti.HasNegligibleHigherPrimePowers.
Removal of the higher prime powers for the standard logarithmic weight. This is the
o(x) corollary of the Layer 5 bound Ο(x) - Ο(x) β€ [K:β] / (2 log 2) Β· βx logΒ² x.
For x β₯ 1, a finite set of primes contributes at most #S Β· log x to Ο. Fibring over
the prime base, the exponents k β₯ 1 with N(π) ^ k β€ x contribute at most log x in total for
each of the finitely many π.
A counting argument can therefore discard a finite exceptional set of primes β those ramifying in
an extension, say, or lying above such β at a cost of O(log x).
The fibre step is TauCeti.card_mul_log_absNorm_le_of_pow_le_of_base_eq, which bounds the total
weight of the prime powers over a single base by log x.
A finite set of primes is O(log x) for Ο, the asymptotic form of the bound above.
A finite set of primes is negligible for Ο, the form the total discard estimate sums.
Transfer of a linear asymptotic from Ο to Ο. If the higher prime powers of S are
negligible and Ο(x) = Ξ΄ x + o(x), then Ο(x) = Ξ΄ x + o(x).
Transfer of a linear asymptotic from Ο to Ο, the converse direction.
The asymptotic-equivalence form of TauCeti.primeTheta_asymptotic_of_primePsi, for a nonzero
density Ξ΄. At Ξ΄ = 0 an equivalence would force Ο to vanish eventually, so the o(x) form
above is the one that covers that case.
The von Mangoldt coefficient system of a set of primes #
The von Mangoldt weight of a set S of height-one primes, as a real weight on the nonzero
integral ideals of π K: the value log N(π) at π ^ k for π β S and k β₯ 1, and 0 at every
other nonzero ideal.
It is the ideal von Mangoldt function of Layer 2 cut down to the prime powers whose base lies in
S, taken in its real form, because the Tauberian input of Layer 9 is a nonnegative real
coefficient system. Cutting down by "some prime of S divides A" rather than by the prime base
of A avoids naming that base at ideals which are not prime powers, where the ideal von Mangoldt
function vanishes anyway.
Equations
- One or more equations did not get rendered due to their size.
Instances For
At an ideal divisible by a prime of S, the von Mangoldt weight of S is the ideal von
Mangoldt value.
The von Mangoldt weight of S vanishes at an ideal with no prime factor in S.
The empty set of primes carries no von Mangoldt weight.
The von Mangoldt weight of S vanishes away from the prime-power ideals.
The von Mangoldt weight of S is nonnegative.
The von Mangoldt weight of S at a positive power of a prime of S.
The von Mangoldt weight of S vanishes at a positive power of a prime outside S.
The von Mangoldt weight is monotone in the set of primes.
The von Mangoldt weight of S on the prime-power carrier is exactly the summand of
Chebyshev's Ο: the standard logarithmic weight at the prime powers with base in S, and 0
elsewhere.
Over all height-one primes the weight is the real form of the ideal von Mangoldt function of Layer 2.
The von Mangoldt coefficient system of a set S of height-one primes: its value at n is
the sum of log N(π) over the prime powers π ^ k of absolute norm exactly n whose base π lies
in S.
This is the nonnegative arithmetic function whose inclusive partial sums are Chebyshev's Ο, by
TauCeti.primePsi_eq_sum_range, and whose Dirichlet series is the one a Tauberian theorem sees.
Equations
- TauCeti.primeVonMangoldtCoeff K S = { toFun := fun (n : β) => β I β TauCeti.normFiber K n, TauCeti.primeVonMangoldtWeight K S I, map_zero' := β― }
Instances For
The von Mangoldt coefficient at n is the total weight of the absolute-norm fibre at n.
The von Mangoldt coefficients are nonnegative, as the Tauberian input requires.
The empty set of primes has vanishing von Mangoldt coefficients.
The von Mangoldt coefficient at 1 vanishes: the unit ideal is the only ideal of absolute
norm one, and it is not a prime power.
The von Mangoldt coefficients are monotone in the set of primes.
The support of the coefficient system: a von Mangoldt coefficient vanishes unless its index is a prime power, since the absolute norm of a prime-power ideal is again a prime power.
The coefficient system is the Layer 1 norm regrouping of the von Mangoldt weight of S,
read in β.
Over all height-one primes the coefficient system regroups the ideal von Mangoldt function of Layer 2 by absolute norm.
Chebyshev's Ο is the inclusive partial sum of the von Mangoldt coefficient system.
This is what lets a Tauberian theorem stated for xβ»ΒΉ β_{n β€ x} a n speak about Ο(x) / x:
Layer 9's conclusion is about the left-hand side, and Layer 10 needs it about the right.
Chebyshev's Ο at a natural cutoff, the form in which the coefficient system is summed.