Counting algebraic numbers of bounded naive height or house

An algebraic number of degree at most d and naive height at most B is a root of an integer polynomial of degree at most d whose coefficients have absolute value at most B. There are at most (2⌊B⌋ + 1)^(d + 1) such polynomials, each with at most d roots, which gives an explicit form of Northcott's theorem for the naive height.

For an algebraic integer the naive height is bounded by a power of the house (TauCeti.naiveHeight_le_two_mul_pow_of_house_le), and the same counting argument, now with monic polynomials, bounds the number of algebraic integers of bounded degree and bounded house.

All statements hold in an arbitrary field of characteristic zero, for instance ℂ or an algebraic closure of ℚ; no complex embedding of the ambient field is needed.

Main results

• TauCeti.finite_setOf_naiveHeight_le: the elements of degree at most d and naive height at most B form a finite set with at most d (2⌊B⌋ + 1)^(d + 1) elements.
• TauCeti.finite_setOf_isIntegral_natDegree_eq_house_le: the algebraic integers of degree exactly k and house at most C form a finite set with at most k (2⌊(2 max(C, 1))ᵏ⌋ + 1)ᵏ elements.
• TauCeti.finite_setOf_isIntegral_house_le: the algebraic integers of degree at most d and house at most C form a finite set with at most ∑ₖ₌₀ᵈ k (2⌊(2 max(C, 1))ᵏ⌋ + 1)ᵏ elements.

References

• J.-H. Evertse, Diophantine Approximation, lecture notes (2019), ch. 1, Theorem 1.7, and ch. 3, Exercise 3.6.

theorem TauCeti.finite_setOf_naiveHeight_le {F : Type u_1} [Field F] [CharZero F] (d : ℕ) (B : ℝ) : {z : F | IsAlgebraic ℚ z ∧ (minpoly ℚ z).natDegree ≤ d ∧ naiveHeight z ≤ B}.Finite ∧ {z : F | IsAlgebraic ℚ z ∧ (minpoly ℚ z).natDegree ≤ d ∧ naiveHeight z ≤ B}.ncard ≤ d * (2 * ⌊B⌋₊ + 1) ^ (d + 1)

Northcott's theorem for the naive height, with Evertse's count. In a field of characteristic zero, the algebraic elements of degree at most d and naive height at most B form a finite set with at most d (2⌊B⌋ + 1)^(d + 1) elements.

theorem TauCeti.finite_setOf_isIntegral_natDegree_eq_house_le {F : Type u_1} [Field F] [CharZero F] (k : ℕ) (C : ℝ) : {z : F | IsIntegral ℤ z ∧ (minpoly ℚ z).natDegree = k ∧ house z ≤ C}.Finite ∧ {z : F | IsIntegral ℤ z ∧ (minpoly ℚ z).natDegree = k ∧ house z ≤ C}.ncard ≤ k * (2 * ⌊(2 * max C 1) ^ k⌋₊ + 1) ^ k

Algebraic integers of exact degree and bounded house, with a count. In a field of characteristic zero, the algebraic integers whose minimal polynomial has degree exactly k and whose house is at most C form a finite set with at most k (2⌊(2 max(C, 1))ᵏ⌋ + 1)ᵏ elements: they are roots of monic integer polynomials of degree k whose lower coefficients are bounded by (2 max(C, 1))ᵏ.

theorem TauCeti.finite_setOf_isIntegral_house_le {F : Type u_1} [Field F] [CharZero F] (d : ℕ) (C : ℝ) : {z : F | IsIntegral ℤ z ∧ (minpoly ℚ z).natDegree ≤ d ∧ house z ≤ C}.Finite ∧ {z : F | IsIntegral ℤ z ∧ (minpoly ℚ z).natDegree ≤ d ∧ house z ≤ C}.ncard ≤ ∑ k ∈ Finset.range (d + 1), k * (2 * ⌊(2 * max C 1) ^ k⌋₊ + 1) ^ k

Finiteness of algebraic integers of bounded house, with a count. In a field of characteristic zero, the algebraic integers of degree at most d and house at most C form a finite set with at most ∑ₖ₌₀ᵈ k (2⌊(2 max(C, 1))ᵏ⌋ + 1)ᵏ elements.