Cancellation in the partial sums of a nontrivial ray class character

Let 𝔪 be a modulus of a number field K and χ a nontrivial ray class character of 𝔪. This file shows that the sum of χ over the nonzero integral ideals prime to 𝔪 of norm at most x is O(x ^ (1 - 1 / [K : ℚ])), in explicit form and in the form O(x ^ (1 - δ)) for some δ > 0.

Main results

• TauCeti.GlobalNumberFields.isBigO_rayClassCharacterPartialSum: the partial sums of a nontrivial ray class character are O(x ^ (1 - 1 / [K : ℚ])).
• TauCeti.GlobalNumberFields.rayClassCharacter_partialSums: the partial sums of a nontrivial ray class character are O(x ^ (1 - δ)) for some δ > 0.

theorem TauCeti.GlobalNumberFields.isBigO_rayClassCharacterPartialSum {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (χ : RayClassCharacter 𝔪) (hχ : χ ≠ 1) : (fun (x : ℝ) => rayClassCharacterPartialSum 𝔪 χ x) =O[Filter.atTop] fun (x : ℝ) => x ^ (1 - (↑(Module.finrank ℚ K))⁻¹)

Cancellation of a nontrivial ray class character, with an explicit power saving. The partial sums of a nontrivial ray class character over the integral ideals of norm at most x are O(x ^ (1 - 1 / [K : ℚ])).

theorem TauCeti.GlobalNumberFields.rayClassCharacter_partialSums {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (χ : RayClassCharacter 𝔪) (hχ : χ ≠ 1) : ∃ (δ : ℝ), 0 < δ ∧ (fun (x : ℝ) => rayClassCharacterPartialSum 𝔪 χ x) =O[Filter.atTop] fun (x : ℝ) => ↑(x ^ (1 - δ))

Cancellation of a nontrivial ray class character. The partial sums of a nontrivial ray class character over the integral ideals of norm at most x are O(x ^ (1 - δ)) for some δ > 0, with the comparison function coerced to ℂ. For the explicit saving δ = 1 / [K : ℚ] against a real comparison function, use isBigO_rayClassCharacterPartialSum.