Counting congruence-lattice points in the ray fundamental domain

Let 𝔪 be a modulus of a number field K and I an invertible fractional ideal. This file counts the points of a coset of congruenceLattice 𝔪 I inside the dilates of the norm-≤-one section of rayFundamentalDomain 𝔪, with a power-saving error and — the point — with an implied constant that does not depend on the coset.

Nothing here is new geometry. The lattice-point count with a power-saving error takes a bounded region whose frontier is Lipschitz parametrizable in codimension one, and the norm-≤-one section of the ray fundamental domain has been shown to be exactly that; the congruence lattice has been shown to be a full ℤ-lattice in the mixed space. This file is the instantiation, and it exists because the three inputs live in three different developments and the fit between them is the step that a count of ideals in a fixed ray class actually consumes.

The count is stated for an arbitrary translate ξ rather than for the lattice itself because a fixed ray class corresponds to one coset of the congruence lattice, so every class needs its own instance of the estimate. What the statement provides is a single A valid for every translate at once, which is the form the class-by-class count consumes directly.

Main results

• TauCeti.GlobalNumberFields.exists_abs_ncard_smul_rayFundamentalDomain_inter_vadd_sub_le: the points of any coset of congruenceLattice 𝔪 I in the dilate c • of the norm-≤-one section number vol / covolume * c ^ [K:ℚ] up to O(c ^ ([K:ℚ] - 1)), uniformly in the coset;
• TauCeti.GlobalNumberFields.exists_abs_ncard_rayFundamentalDomain_inter_norm_le_inter_vadd_sub_le — the same count graded by the norm: the main term is linear in t and the error is O(t ^ (1 - 1 / [K:ℚ])).

References

• S. Lang, Algebraic Number Theory, Chapter VI, §2.

theorem TauCeti.GlobalNumberFields.exists_abs_ncard_smul_rayFundamentalDomain_inter_vadd_sub_le {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) : ∃ A ≥ 0, ∀ (ξ : NumberField.mixedEmbedding.mixedSpace K) (c : ℝ), 1 ≤ c → |↑(c • (rayFundamentalDomain 𝔪 ∩ {x : NumberField.mixedEmbedding.mixedSpace K | NumberField.mixedEmbedding.norm x ≤ 1}) ∩ (ξ +ᵥ ↑(congruenceLattice 𝔪 I))).ncard - MeasureTheory.volume.real (rayFundamentalDomain 𝔪 ∩ {x : NumberField.mixedEmbedding.mixedSpace K | NumberField.mixedEmbedding.norm x ≤ 1}) / ZLattice.covolume (congruenceLattice 𝔪 I) MeasureTheory.volume * c ^ Module.finrank ℝ (NumberField.mixedEmbedding.mixedSpace K)| ≤ A * c ^ (Module.finrank ℝ (NumberField.mixedEmbedding.mixedSpace K) - 1)

The congruence-lattice count in the ray fundamental domain, uniformly in the coset. For any coset ξ +ᵥ congruenceLattice 𝔪 I, the number of its points in the dilate c • (rayFundamentalDomain 𝔪 ∩ {norm ≤ 1}) is the volume ratio times c ^ [K:ℚ], with an error O(c ^ ([K:ℚ] - 1)) whose implied constant is independent of both c and the coset.

The exponent is written finrank ℝ (mixedSpace K), which is [K:ℚ] by NumberField.mixedEmbedding.finrank; a consumer counting ideals by their absolute norm rewrites along that equality.

theorem TauCeti.GlobalNumberFields.exists_abs_ncard_rayFundamentalDomain_inter_norm_le_inter_vadd_sub_le {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) : ∃ A ≥ 0, ∀ (ξ : NumberField.mixedEmbedding.mixedSpace K) (t : ℝ), 1 ≤ t → |↑(rayFundamentalDomain 𝔪 ∩ {x : NumberField.mixedEmbedding.mixedSpace K | NumberField.mixedEmbedding.norm x ≤ t} ∩ (ξ +ᵥ ↑(congruenceLattice 𝔪 I))).ncard - MeasureTheory.volume.real (rayFundamentalDomain 𝔪 ∩ {x : NumberField.mixedEmbedding.mixedSpace K | NumberField.mixedEmbedding.norm x ≤ 1}) / ZLattice.covolume (congruenceLattice 𝔪 I) MeasureTheory.volume * t| ≤ A * t ^ (1 - (↑(Module.finrank ℚ K))⁻¹)

The congruence-lattice count graded by the norm, uniformly in the coset. For any coset ξ +ᵥ congruenceLattice 𝔪 I, the number of its points in the ray fundamental domain of norm at most t is vol / covolume * t, with an error O(t ^ (1 - 1 / [K:ℚ])) whose implied constant is independent of both t and the coset.

This is the previous estimate regraded from dilations to norms: the main term is linear in t, and the boundary exponent [K:ℚ] - 1 becomes the power saving 1 / [K:ℚ]. Unlike ZLattice.covolume.tendsto_card_le_div', which gives a limit, it provides an explicit error term, uniform in the coset.