The Perron formula for sums over ideals #
Let f be an arithmetic function on the nonzero ideals of the ring of integers of a number field
K, and let the L-series of its norm coefficients TauCeti.normCoeff K f converge absolutely on
the line Re s = c > 0. This file reads the arithmetic Perron formula of
TauCeti/NumberTheory/ArithmeticDirichletSeries/Perron/Formula.lean as a statement about the
ideal sums ∑_{N(I) ≤ x} f(I) themselves.
The sharp step TauCeti.perronStep gives an ideal I with N(I) ≤ x the weight 1 when
N(I) < x and the weight 1 / 2 when N(I) = x, so the limit of the truncated Perron integral
is the finite ideal sum ∑_{N(I) ≤ x} f(I) perronStep (x / N(I))
(TauCeti.tsum_normCoeff_mul_perronStep). It is the inclusive summatory function
TauCeti.idealSummatory K f x exactly when x is not the norm of a nonzero ideal, and at an
integer endpoint x = N every ideal of norm N enters with half weight, so that the limit is
∑_{N(I) ≤ N} f(I) - normCoeff K f N / 2.
Only nonzero norm coefficients matter at endpoints. An integer x for which normCoeff K f x = 0
behaves like a non-integer, even when ideals of norm x exist. The off-norm statements are
corollaries for endpoints that are not norms of nonzero ideals.
Main results #
TauCeti.perronFormula: the truncated Perron integral of theL-series of the norm coefficients tends to the step-weighted ideal sum∑_{N(I) ≤ x} f(I) perronStep (x / N(I)).TauCeti.perronFormula_of_forall_normCoeff_ne: when the norm coefficient at any possible endpoint vanishes, the limit isTauCeti.idealSummatory K f x.TauCeti.perronFormula_of_forall_absNorm_ne: off the norms the limit isTauCeti.idealSummatory K f x.TauCeti.perronFormula_natCast: at an integer endpointNthe limit isTauCeti.idealSummatory K f N - normCoeff K f N / 2, the ideals of normNentering with half weight.TauCeti.norm_truncatedPerron_LSeries_normCoeff_sub_idealSummatory_le: off the norms, the truncated integral at finite height differs fromTauCeti.idealSummatory K f xby at most the series of the smoothed-step kernel errors. Its_of_forall_normCoeff_nevariant only requires nonzero norm coefficients to avoid the endpoint.
References #
- H. Davenport, Multiplicative Number Theory, chapter 17.
- J. Neukirch, Algebraic Number Theory, Chapter VII.
The Perron step series of the norm coefficients is a finite ideal sum. Every index above
x has step weight 0, and the norm fibre at each index below it redistributes the weight over
the ideals of that norm.
Off the norms the step weights are sharp. If x is not the absolute norm of any nonzero
ideal, every ideal counted up to x has norm strictly below x, and so step weight 1.
The half weight at an integer endpoint. At x = N the ideals of norm N receive step
weight 1 / 2 and all others counted up to N receive 1, so the step-weighted sum is the
inclusive ideal sum less half of the norm coefficient at N.
The step-weighted ideal sum equals the inclusive sum whenever the norm coefficient at a possible endpoint vanishes.
The arithmetic Perron formula for ideal sums. Where the L-series of the norm
coefficients of f converges absolutely on the line Re s = c, the truncated Perron integral
tends, as the height grows, to the ideal sum ∑_{N(I) ≤ x} f(I) in which each ideal of norm
exactly x carries half weight. The two readings of this limit are
TauCeti.perronFormula_of_forall_absNorm_ne and TauCeti.perronFormula_natCast.
The Perron formula when every nonzero norm coefficient is away from the endpoint.
The Perron formula off the norms. If x > 0 is not the absolute norm of a nonzero ideal,
the truncated Perron integral tends to the inclusive ideal sum ∑_{N(I) ≤ x} f(I).
The Perron formula at an integer endpoint. At x = N the truncated Perron integral tends
to the inclusive ideal sum ∑_{N(I) ≤ N} f(I) less half of the norm coefficient at N: every
ideal of norm exactly N enters with half weight.
The truncated Perron error bound when every nonzero norm coefficient is away from the endpoint.
The truncated Perron formula off the norms. If x > 0 is not the absolute norm of a
nonzero ideal, then at every positive height T the truncated Perron integral differs from the
inclusive ideal sum ∑_{N(I) ≤ x} f(I) by at most the series of the smoothed-step kernel errors at
the ratios x / n.