Counting ideals of bounded norm

TheoremBound on the number of ideals of bounded norm, integer threshold#✓fully proved

Let \(K\) be a number field of degree \(n = [K : \mathbb{Q}]\) with ring of integers \(\mathcal{O}_K\), let \(M\) be a natural number, and let \(k\) be the largest natural number with \(2^k \le M\), with \(k = 0\) if \(M = 0\). Then the number of nonzero ideals \(I\) of \(\mathcal{O}_K\) whose absolute norm \(N(I) = |\mathcal{O}_K / I|\) satisfies \(N(I) \le M\) is at most \((nM)^k\).

theorem card_nonzero_absNorm_le (M : ℕ) :
    Nat.card {I : Ideal (𝓞 K) // I ≠ ⊥ ∧ Ideal.absNorm I ≤ M} ≤
      (Module.finrank ℚ K * M) ^ Nat.log 2 M

Sources

• ATLAS NumberTheoryI:295, Number Theory I, Section 14.5, Lemma 14.21; this is a discrete strengthening with an integer threshold, valid also at \(M = 0\) and \(M = 1\), not the source's literal positive-real statement.

Used by 1

Used byBound on the number of ideals of bounded norm, floor form

TheoremBound on the number of ideals of bounded norm, floor form#✓fully proved

Let \(K\) be a number field of degree \(n = [K : \mathbb{Q}]\) with ring of integers \(\mathcal{O}_K\), let \(M\) be any real number, and let \(m = \max(0, \lfloor M \rfloor)\). Let \(k\) be the largest natural number with \(2^k \le m\), and \(k = 0\) if \(m = 0\). Then the number of nonzero ideals \(I\) of \(\mathcal{O}_K\) whose absolute norm \(N(I) = |\mathcal{O}_K / I|\) satisfies \(N(I) \le M\) is at most \((nm)^k\).

For \(M < 1\) there are no such ideals, since every nonzero ideal has norm at least \(1\); for \(M \ge 1\) the condition \(N(I) \le M\) is equivalent to \(N(I) \le m\).

theorem card_nonzero_absNorm_le_real (M : ℝ) :
    Nat.card {I : Ideal (𝓞 K) // I ≠ ⊥ ∧ (Ideal.absNorm I : ℝ) ≤ M} ≤
      (Module.finrank ℚ K * ⌊M⌋₊) ^ Nat.log 2 ⌊M⌋₊

Uses 1 · Used by 1

Proof usesBound on the number of ideals of bounded norm, integer threshold

Used byBound on the number of ideals of bounded norm

TheoremBound on the number of ideals of bounded norm#✓fully proved

Let \(K\) be a number field of degree \(n = [K : \mathbb{Q}]\) with ring of integers \(\mathcal{O}_K\), and let \(M > 0\) be a real number. The number of nonzero ideals \(I\) of \(\mathcal{O}_K\) whose absolute norm \(N(I) = |\mathcal{O}_K / I|\) satisfies \(N(I) \le M\) is at most \((nM)^{\log_2 M}\), where the exponent \(\log_2 M\) is a real number.

theorem card_nonzero_absNorm_le_real_rpow (M : ℝ) (hM : 0 < M) :
    (Nat.card {I : Ideal (𝓞 K) //
      I ≠ ⊥ ∧ (Ideal.absNorm I : ℝ) ≤ M} : ℝ) ≤
      ((Module.finrank ℚ K : ℝ) * M) ^ (Real.logb 2 M)

Sources

• ATLAS NumberTheoryI:295, Number Theory I, Section 14.5, Lemma 14.21. The proof derives this bound from the integer-threshold and floor variants.

Uses 1

Proof usesBound on the number of ideals of bounded norm, floor form

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.