An effective count of ideals of bounded norm

In a number field F of degree n, the number of nonzero integral ideals of norm at most X is at most X² · 2ⁿ. A nonzero ideal is encoded injectively as an n-tuple of positive naturals with product ≤ absNorm I (distributing, for each rational prime p, the value p^{vₚ} of the i-th prime above p into the i-th coordinate); the valuations of the tuple recover the ideal, and there are at most X²·2ⁿ such tuples.

Mathlib's Ideal.finite_setOfPred_absNorm_le already gives finiteness (and Ideal/Asymptotics the sharp asymptotic ~ ρ·X); the contribution here is the explicit elementary bound, the input to the effective class-number estimate.

Main result

• NumberField.card_ideal_absNorm_le: at most X²·2^[F:ℚ] nonzero ideals of norm ≤ X.

The Consumer section at the end restates this bound in the natural-number and degree-monotone forms later effective estimates use (ncard_ideal_absNorm_le_nat, ncard_ideal_absNorm_le_of_nat_le_of_finrank_le, ncard_ideal_absNorm_le_of_finrank_le, ncard_ideal_absNorm_le_nat_of_finrank_le).

Provenance

Migrated from kim-em/erdos-unit-distance, the formalization of L. Alpöge's disproof of the uniform-constant Erdős unit-distance conjecture, where this Rankin-style count fed the class-number bound.

Encoding ideals as tuples (for the Rankin-style ideal count)

We encode a nonzero ideal I of 𝓞 F as an n-tuple of positive naturals (n = [F:ℚ]) whose product is at most absNorm I, injectively. For a nonzero prime P, absNormUnder P is the norm of the rational prime below P and primeCoord P is the index of P among the (at most n) primes above that rational prime. The i-th coordinate of the encoding multiplies (absNormUnder P) ^ (mult of P in I) over all prime factors P of I with primeCoord P = i.

theorem NumberField.card_ideal_absNorm_le (F : Type u_1) [Field F] [NumberField F] {X : ℝ} (hX : 1 ≤ X) : {I : Ideal (RingOfIntegers F) | I ≠ ⊥ ∧ ↑(Ideal.absNorm I) ≤ X}.Finite ∧ ↑{I : Ideal (RingOfIntegers F) | I ≠ ⊥ ∧ ↑(Ideal.absNorm I) ≤ X}.ncard ≤ X ^ 2 * 2 ^ Module.finrank ℚ F

In any number field F, the set of nonzero integral ideals with norm at most X is finite, and for X ≥ 1 its cardinality is at most X² * 2^[F:ℚ].

Consumer forms

These are direct corollaries of card_ideal_absNorm_le, packaging its real norm bound as the natural-number and degree-monotone forms that later effective estimates carry.

theorem NumberField.ncard_ideal_absNorm_le_nat (F : Type u_1) [Field F] [NumberField F] (N : ℕ) : {I : Ideal (RingOfIntegers F) | I ≠ ⊥ ∧ Ideal.absNorm I ≤ N}.ncard ≤ N ^ 2 * 2 ^ Module.finrank ℚ F

Natural-number ideal count. The number of nonzero integral ideals of 𝓞 F with norm at most N is at most N² * 2^[F:ℚ].

theorem NumberField.ncard_ideal_absNorm_le_of_finrank_le (F : Type u_1) [Field F] [NumberField F] {X : ℝ} {n : ℕ} (hX : 1 ≤ X) (hn : Module.finrank ℚ F ≤ n) : ↑{I : Ideal (RingOfIntegers F) | I ≠ ⊥ ∧ ↑(Ideal.absNorm I) ≤ X}.ncard ≤ X ^ 2 * 2 ^ n

If 1 ≤ X and [F : ℚ] ≤ n, then the number of nonzero integral ideals of norm at most X is at most X² * 2^n. This is the degree-monotone form of NumberField.card_ideal_absNorm_le.

theorem NumberField.ncard_ideal_absNorm_le_of_nat_le_of_finrank_le (F : Type u_1) [Field F] [NumberField F] {N B n : ℕ} (hN : N ≤ B) (hn : Module.finrank ℚ F ≤ n) : {I : Ideal (RingOfIntegers F) | I ≠ ⊥ ∧ Ideal.absNorm I ≤ N}.ncard ≤ B ^ 2 * 2 ^ n

Monotone natural-number ideal count: if all ideals under consideration have norm at most N, and N ≤ B, and [F : ℚ] ≤ n, then there are at most B² * 2^n of them.

theorem NumberField.ncard_ideal_absNorm_le_nat_of_finrank_le (F : Type u_1) [Field F] [NumberField F] {N n : ℕ} (hn : Module.finrank ℚ F ≤ n) : {I : Ideal (RingOfIntegers F) | I ≠ ⊥ ∧ Ideal.absNorm I ≤ N}.ncard ≤ N ^ 2 * 2 ^ n

If [F : ℚ] ≤ n, then the number of nonzero integral ideals of norm at most N is at most N² * 2^n.