Cancellation in ideal partial sums and the continued L-function of a weight #
For a unitary ideal weight χ of a number field K of degree d = [K : ℚ], the partial sums
∑_{N(I) ≤ x} χ(I) over the nonzero integral ideals are trivially O(x), by the linear ideal
count. For nontrivial finite-order ray class characters, equidistribution among ray classes gives
the stronger bound O(x ^ (1 - 1 / d)). This file names that bound as a hypothesis and extracts
its analytic consequence.
TauCeti.HasCancellation χis the uniform bound‖∑_{N(I) ≤ x} χ(I)‖ ≤ C * x ^ (1 - 1 / d)for every real cutoffx ≥ 1, with the inclusive summatory functionTauCeti.idealSummatory. Equivalently (TauCeti.hasCancellation_iff_isBigO), the partial sums areO(x ^ (1 - 1 / d))asx → ∞.TauCeti.continuedLFunctionOfWeight χis the partial-summation integrals * ∫_{1}^{∞} (∑_{N(I) ≤ t} χ(I)) t ^ (-(s + 1)) dt.
It agrees with the norm-regrouped L-series of χ on Re s > 1 for every unitary weight
(TauCeti.continuedLFunctionOfWeight_eq_LSeries), and under HasCancellation χ it is holomorphic
on Re s > 1 - 1 / d (TauCeti.differentiableOn_continuedLFunctionOfWeight); so it is an analytic
continuation of the L-series of χ across the line Re s = 1.
Both are stable under deleting finitely many Euler factors, the operation a character family
needs at the bad primes of its modulus. A one-prime recurrence relates the partial sums after
inserting a forbidden prime to two partial sums before the insertion
(TauCeti.MultiplicativeIdealWeight.idealSummatory_restrict_insert). Iterating this recurrence
shows that cancellation passes to the restriction (TauCeti.HasCancellation.restrict); on
Re s > 1 the two continued
L-functions differ by the entire factor ∏ 𝔭 ∈ S, (1 - χ(𝔭) N(𝔭) ^ (-s))
(TauCeti.continuedLFunctionOfWeight_restrict_of_one_lt_re), and under cancellation that identity
propagates to the whole half-plane Re s > 1 - 1 / d
(TauCeti.continuedLFunctionOfWeight_restrict).
In number-field degree greater than one, cancellation is also invariant under purely imaginary
norm twists (TauCeti.hasCancellation_normTwist_iff). Abel summation supplies this because the
cancellation exponent 1 - 1 / [K : ℚ] is then positive. The degree-one case is deliberately not
claimed: the defining bound has exponent zero, while the absolute bound for the Abel integral is
logarithmic.
The continued L-function itself follows these operations. Conjugating the weight reflects it
in the real axis, L(conj χ, conj s) = conj (L(χ, s)), at every s
(TauCeti.continuedLFunctionOfWeight_conj). An imaginary norm twist by N(I) ^ (-z) translates
it by z: on Re s > 1 for every weight
(TauCeti.continuedLFunctionOfWeight_normTwist_of_one_lt_re), and on the whole half-plane
Re s > 1 - 1 / d when both the weight and its twist have cancellation
(TauCeti.continuedLFunctionOfWeight_normTwist).
Cancellation is a hypothesis about the partial sums themselves. It cannot be replaced by
finiteness of the image of χ or of a quotient through which it factors: the values of a weight
factoring through a finite quotient of the free group on the prime ideals can be prescribed
arbitrarily prime by prime.
Nor is it automatic, and TauCeti.not_hasCancellation_of_isNormTwistOnGood says which weights it
excludes: those agreeing with a norm twist I ↦ N(I) ^ (u * I) on the ideals prime to their bad
primes. The L-series of such a weight is the Dedekind zeta function with finitely many Euler
factors deleted, read at s - u * I, so it has a pole at s = 1 + u * I, where cancellation
would instead make continuedLFunctionOfWeight χ holomorphic. The trivial weight
(TauCeti.not_hasCancellation_one) and its purely imaginary norm twists
(TauCeti.not_hasCancellation_normTwist_one) are the cases a character-family argument meets:
it must not assume cancellation for the degenerate members of its family.
References #
- H. Davenport, Multiplicative Number Theory, Chapter 1 (partial summation).
- G. Tenenbaum, Introduction to Analytic and Probabilistic Number Theory, Chapter II.1.
- J. Neukirch, Algebraic Number Theory, Chapter VII §6, for the partial-sum bound of finite-order ray class character L-series.
Cancellation in the ideal partial sums of a unitary weight. There is a constant C with
‖∑_{N(I) ≤ x} χ(I)‖ ≤ C * x ^ (1 - 1 / [K : ℚ]) for every real cutoff x ≥ 1, the sum running
over the nonzero integral ideals of absolute norm at most x.
Equations
- TauCeti.HasCancellation χ = ∃ (C : ℝ), ∀ (x : ℝ), 1 ≤ x → ‖TauCeti.idealSummatory K χ.toIdealArithmeticFunction x‖ ≤ C * x ^ (1 - 1 / ↑(Module.finrank ℚ K))
Instances For
The cancellation exponent 1 - 1 / [K : ℚ] is less than 1.
Cancellation is an asymptotic bound. A weight has cancellation exactly when its ideal
partial sums are O(x ^ (1 - 1 / [K : ℚ])) as x → ∞: on any bounded range of cutoffs x ≥ 1
the partial sums are bounded by an ideal count, so the eventual bound is uniform.
The ideal partial sums of the conjugate of a unitary weight are the complex conjugates of the partial sums of the weight.
A weight has cancellation exactly when its complex conjugate does: conjugation commutes with the finite partial sums and preserves their modulus.
Cancellation survives an imaginary norm twist in number-field degree greater than one.
If the ideal partial sums of χ are O(x ^ (1 - 1 / [K : ℚ])), then multiplying the value
at an ideal I by N(I) ^ (-z) for Re z = 0 preserves the same bound, provided [K : ℚ] > 1.
The degree hypothesis is exactly what makes the cancellation exponent positive: Abel summation
bounds the integral term by a constant times x ^ (1 - 1 / [K : ℚ]).
Cancellation is invariant under imaginary norm twists in degree greater than one.
Cancellation may be transported freely across an imaginary norm twist in either direction, so a
character-family argument can normalize away such a twist when [K : ℚ] > 1.
Deleting finitely many Euler factors #
Cancellation survives the deletion of finitely many Euler factors. If the ideal partial
sums of a unitary weight χ are O(x ^ (1 - 1 / [K : ℚ])), so are those of its restriction away
from a finite set of primes: each prime removed splits the partial sum into two partial sums of
the same order, at the cutoffs x and x / N(𝔭).
Character-family arguments use this to pass between a weight and the one whose Euler factors at a finite set of bad primes have been deleted.
Cancellation bounds the partial sums of the norm coefficients, in the O(n ^ r) form of
Mathlib's LSeries_eq_mul_integral.
The continued L-function of a unitary weight, defined by partial summation:
s * ∫_{1}^{∞} (∑_{N(I) ≤ t} χ(I)) t ^ (-(s + 1)) dt.
On Re s > 1 it is the norm-regrouped L-series of χ
(TauCeti.continuedLFunctionOfWeight_eq_LSeries); under TauCeti.HasCancellation χ it is
holomorphic on Re s > 1 - 1 / [K : ℚ] (TauCeti.differentiableOn_continuedLFunctionOfWeight).
Where the integral does not converge it takes the junk value of Mathlib's Bochner integral.
Equations
- TauCeti.continuedLFunctionOfWeight χ s = s * ∫ (t : ℝ) in Set.Ioi 1, TauCeti.idealSummatory K χ.toIdealArithmeticFunction t * ↑t ^ (-(s + 1))
Instances For
The continued L-function as the integral of Mathlib's LSeries_eq_mul_integral, over the
partial sums of the norm coefficients.
The continued L-function is the L-series on Re s > 1. For every unitary weight, with or
without cancellation, continuedLFunctionOfWeight χ agrees with the LSeries of the norm
coefficients of χ to the right of 1, where that series converges absolutely.
Cancellation continues the L-series of a weight. If χ has cancellation, its continued
L-function is holomorphic on the half-plane Re s > 1 - 1 / [K : ℚ], which contains the line
Re s = 1.
Holomorphy on the closed half-plane Re s ≥ 1. Under cancellation the continued
L-function of χ is complex differentiable at every point of Re s ≥ 1, which lies inside the
half-plane Re s > 1 - 1 / [K : ℚ] of TauCeti.differentiableOn_continuedLFunctionOfWeight.
Deleting finitely many Euler factors, to the right of 1. Where the norm-regrouped series
converge absolutely, restricting a unitary weight away from a finite set S of primes multiplies
its continued L-function by the reciprocals ∏ 𝔭 ∈ S, (1 - χ(𝔭) N(𝔭) ^ (-s)) of the deleted
local factors.
Deleting finitely many Euler factors, across the line Re s = 1. Under cancellation both
sides of TauCeti.continuedLFunctionOfWeight_restrict_of_one_lt_re are holomorphic on the
half-plane Re s > 1 - 1 / [K : ℚ], which is connected, so the identity propagates there from
the half-plane Re s > 1 where it was proved. The correction factor is entire.
Conjugation and imaginary norm twists #
The continued L-function of the conjugate weight is the reflection of the continued
L-function of the weight in the real axis: L(conj χ, conj s) = conj (L(χ, s)).
This holds at every s,
including the junk values off the region where the defining integral converges, because complex
conjugation commutes with the Bochner integral.
Imaginary norm twists translate the continued L-function, to the right of 1. Twisting
a unitary weight by N(I) ^ (-z) with Re z = 0 translates its continued L-function by z on
the half-plane Re s > 1, where both sides are the norm-regrouped L-series.
Imaginary norm twists translate the continued L-function, across the line Re s = 1.
If both a unitary weight and its twist by N(I) ^ (-z), with Re z = 0, have cancellation,
then the continued L-function of the twist at s is the continued L-function of the weight at
s + z, throughout the half-plane Re s > 1 - 1 / [K : ℚ].
In degree [K : ℚ] > 1 the second cancellation hypothesis follows from the first, by
TauCeti.HasCancellation.normTwist.
The rejection test: weights that are norm twists on their good ideals #
A weight that is a norm twist on its good ideals has no cancellation. Its norm
coefficients are those of the indicator of the ideals prime to its bad primes, twisted by
n ^ (u * I), so its L-series is the Dedekind zeta function with finitely many Euler factors
deleted, read at s - u * I. That series has a pole at s = 1 + u * I, a point at which
cancellation would make TauCeti.continuedLFunctionOfWeight holomorphic.
This is a rejection test for character-family arguments: these weights are degenerate examples for which cancellation may not be assumed.
A weight that is trivial on its good ideals has no cancellation: its L-series is the
Dedekind zeta function with finitely many Euler factors deleted, which has a pole at s = 1.
The trivial weight has no cancellation. Its L-series is the Dedekind zeta function,
which has a pole at s = 1.
No imaginary norm twist of the trivial weight has cancellation. Its L-series is the
Dedekind zeta function read at s + z, which has a pole at s = 1 - z.