Character sums over the integral ideals of bounded norm

Let 𝔪 be a modulus of a number field K and χ a ray class character of 𝔪. This file introduces rayClassCharacterPartialSum 𝔪 χ x, the sum of χ over the nonzero integral ideals prime to the finite part of 𝔪 whose norm is at most x, and identifies it with the χ-weighted combination of the ray class counting functions.

The sum ranges over ideals, not over chosen class representatives. Regrouping it by ray class is exactly the partition idealClassSigmaEquiv, and on each fibre χ is constant, so each class contributes its counting function scaled by the single value χ takes there.

Main definitions

• TauCeti.GlobalNumberFields.rayClassCharacterPartialSum: the partial sum of a ray class character over the integral ideals of bounded norm.

Main results

• TauCeti.GlobalNumberFields.rayClassCharacterPartialSum_eq_sum: the partial sum is ∑ c, χ c * rayClassIdealCountingFunction 𝔪 c x.

noncomputable def TauCeti.GlobalNumberFields.rayClassCharacterPartialSum {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (χ : RayClassCharacter 𝔪) (x : ℝ) : ℂ

The partial sum of a ray class character. The inclusive summatory function, in the sense of TauCeti.summatory, of χ.onIdeals over the nonzero integral ideals prime to the finite part of 𝔪, graded by the absolute norm.

theorem TauCeti.GlobalNumberFields.rayClassCharacterPartialSum_def {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (χ : RayClassCharacter 𝔪) (x : ℝ) : rayClassCharacterPartialSum 𝔪 χ x = ∑ᶠ (I : { I : ↥(integralIdealsPrimeTo 𝔪) // ↑(Ideal.absNorm ↑I) ≤ x }), ↑(χ.onIdeals ↑I)

The partial sum as the finsum defining it. The rewrite rule turning rayClassCharacterPartialSum into the sum of χ.onIdeals over the integral ideals prime to 𝔪 of norm at most x.

theorem TauCeti.GlobalNumberFields.rayClassCharacterPartialSum_eq_sum {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) [Fintype (RayClassGroup 𝔪)] (χ : RayClassCharacter 𝔪) (x : ℝ) : rayClassCharacterPartialSum 𝔪 χ x = ∑ c : RayClassGroup 𝔪, ↑(χ c) * ↑(rayClassIdealCountingFunction 𝔪 c x)

A character partial sum is the weighted combination of the class counts. The partial sum of χ over the integral ideals prime to 𝔪 of norm at most x is the sum of the ray class counting functions, each weighted by the value χ takes on its class.