The asymptotic count of the integral ideals of a ray class

Let 𝔪 be a modulus of a number field K of degree n. This file proves that the number of nonzero integral ideals prime to 𝔪 in a fixed ray class with absolute norm at most x is rayClassIdealMainTerm 𝔪 * x + O(x ^ (1 - 1 / n)), with the same main term and the same power saving for every class.

Main results

• TauCeti.GlobalNumberFields.isBigO_rayClassIdealCountingFunction_sub: the ray class ideal counting function of a class is rayClassIdealMainTerm 𝔪 * x + O(x ^ (1 - 1 / [K : ℚ])).
• TauCeti.GlobalNumberFields.rayClassIdealCount: the ray class ideal counting function is rayClassIdealMainTerm 𝔪 * x + O(x ^ (1 - δ)) for some δ > 0 uniform in the class.

theorem TauCeti.GlobalNumberFields.isBigO_rayClassIdealCountingFunction_sub {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (c : RayClassGroup 𝔪) : (fun (x : ℝ) => ↑(rayClassIdealCountingFunction 𝔪 c x) - rayClassIdealMainTerm 𝔪 * x) =O[Filter.atTop] fun (x : ℝ) => x ^ (1 - (↑(Module.finrank ℚ K))⁻¹)

The ray class ideal count of a single class, with an explicit power saving. The number of nonzero integral ideals prime to 𝔪 in the ray class c with norm at most x is rayClassIdealMainTerm 𝔪 * x + O(x ^ (1 - 1 / [K : ℚ])).

theorem TauCeti.GlobalNumberFields.rayClassIdealCount {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (c : RayClassGroup 𝔪), (fun (x : ℝ) => ↑(rayClassIdealCountingFunction 𝔪 c x) - rayClassIdealMainTerm 𝔪 * x) =O[Filter.atTop] fun (x : ℝ) => x ^ (1 - δ)

The ray class ideal count. For every modulus 𝔪 there is a power saving δ > 0 such that, in each ray class c of 𝔪, the number of nonzero integral ideals prime to 𝔪 of norm at most x is rayClassIdealMainTerm 𝔪 * x + O(x ^ (1 - δ)). One can take δ = 1 / [K : ℚ]; for that explicit exponent, use isBigO_rayClassIdealCountingFunction_sub instead.

theorem TauCeti.GlobalNumberFields.tendsto_rayClassIdealCountingFunction_div {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (c : RayClassGroup 𝔪) : Filter.Tendsto (fun (x : ℝ) => ↑(rayClassIdealCountingFunction 𝔪 c x) / x) Filter.atTop (nhds (rayClassIdealMainTerm 𝔪))

In every ray class the count divided by x tends to the main term. The power saving of rayClassIdealCount is negligible against x.