Cancellation for the ideal weight of a ray class character

The ideal partial sums of the unitary weight χ.toUnitaryIdealWeight of a ray class character χ of 𝔪 are the character sums rayClassCharacterPartialSum 𝔪 χ: the weight vanishes on the ideals that are not prime to 𝔪 and is χ of the ray class on the others. For a nontrivial character those sums are O(x ^ (1 - 1 / [K : ℚ])), which is the cancellation hypothesis TauCeti.HasCancellation of the Arithmetic Dirichlet Series library. Through TauCeti.differentiableOn_continuedLFunctionOfWeight it continues the L-series of a nontrivial ray class character holomorphically to Re s > 1 - 1 / [K : ℚ], a half-plane containing the line Re s = 1.

Main results

• TauCeti.GlobalNumberFields.RayClassCharacter.idealSummatory_toUnitaryIdealWeight: the ideal partial sums of the weight are the character sums.
• TauCeti.GlobalNumberFields.RayClassCharacter.hasCancellation_toUnitaryIdealWeight: the weight of a nontrivial ray class character has cancellation.

Implementation notes

The reindexing proof of idealSummatory_toUnitaryIdealWeight is adapted from the private lemma idealSummatory_restrictAway_galoisCharacterUnitaryWeight formerly in TauCeti/NumberTheory/Chebotarev/GaloisCharacter/Cyclotomic/Cancellation.lean, which now derives its cancellation from hasCancellation_toUnitaryIdealWeight instead.

References

• J. Neukirch, Algebraic Number Theory, Chapter VII, §6 and §8.

theorem TauCeti.GlobalNumberFields.RayClassCharacter.idealSummatory_toUnitaryIdealWeight {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} (χ : RayClassCharacter 𝔪) (x : ℝ) : idealSummatory K χ.toUnitaryIdealWeight.toIdealArithmeticFunction x = rayClassCharacterPartialSum 𝔪 χ x

The ideal partial sums of a ray class weight are the character sums. Summing the unitary weight of χ over the nonzero ideals of norm at most x gives the sum of χ over the integral ideals prime to 𝔪 of norm at most x, since the weight vanishes on the other ideals.

theorem TauCeti.GlobalNumberFields.RayClassCharacter.hasCancellation_toUnitaryIdealWeight {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {χ : RayClassCharacter 𝔪} (hχ : χ ≠ 1) : HasCancellation χ.toUnitaryIdealWeight

Cancellation for a nontrivial ray class character. The unitary weight of a nontrivial ray class character has ideal partial sums O(x ^ (1 - 1 / [K : ℚ])).