Denominators and the size of an algebraic number

The denominator den(x) = Algebra.natDenominator x of an algebraic number x is the least positive integer D such that D x is an algebraic integer: it generates the ideal of integers clearing the denominator of x (Algebra.natDenominator_dvd_iff), and it is 1 exactly for an algebraic integer (Algebra.natDenominator_eq_one_iff). It divides the leading coefficient of the primitive minimal polynomial of x (TauCeti.natDenominator_dvd_leadingCoeff_primitiveMinpoly), which is at most its d-th power (TauCeti.leadingCoeff_primitiveMinpoly_le_natDenominator_pow).

The main result is Evertse's lower bound for the conjugates of a nonzero algebraic number: for an algebraic z of degree d over ℚ in a field of characteristic zero and every complex conjugate w of z,

den(z) ^ d * house(z) ^ (d - 1) * ‖w‖ ≥ 1,

that is, ‖w‖ ≥ den(z) ^ (-d) * house(z) ^ (1 - d) (TauCeti.one_le_natDenominator_pow_mul_house_pow_mul_norm_of_mem_rootSet); the form with integer powers is stated at w = z (TauCeti.zpow_natDenominator_mul_zpow_house_le_norm). The leading coefficient of the primitive minimal polynomial satisfies the sharper bound TauCeti.one_le_leadingCoeff_primitiveMinpoly_mul_house_pow_mul_norm. For an algebraic integer the denominator is 1, so the bound reads house(z) ^ (d - 1) * ‖w‖ ≥ 1 for every conjugate w (TauCeti.one_le_house_pow_mul_norm_of_mem_rootSet).

References

• J.-H. Evertse, Diophantine Approximation, lecture notes (2019), ch. 3, Exercise 3.7, p. 60.

theorem TauCeti.one_le_leadingCoeff_primitiveMinpoly_mul_house_pow_mul_norm {K : Type u_1} [Field K] [CharZero K] {z : K} {w : ℂ} (hz : IsAlgebraic ℚ z) (hz0 : z ≠ 0) (hw : w ∈ (minpoly ℚ z).rootSet ℂ) : 1 ≤ ↑(primitiveMinpoly z).leadingCoeff * house z ^ ((minpoly ℚ z).natDegree - 1) * ‖w‖

The conjugate bound in terms of the leading coefficient. Let z be a nonzero algebraic number of degree d in a field of characteristic zero and let a₀ be the leading coefficient of its primitive minimal polynomial. Every complex conjugate w of z satisfies a₀ * house(z) ^ (d - 1) * ‖w‖ ≥ 1.

theorem TauCeti.one_le_natDenominator_pow_mul_house_pow_mul_norm_of_mem_rootSet {K : Type u_1} [Field K] [CharZero K] {z : K} {w : ℂ} (hz : IsAlgebraic ℚ z) (hz0 : z ≠ 0) (hw : w ∈ (minpoly ℚ z).rootSet ℂ) : 1 ≤ ↑(Algebra.natDenominator z) ^ (minpoly ℚ z).natDegree * house z ^ ((minpoly ℚ z).natDegree - 1) * ‖w‖

Evertse's lower bound for the conjugates of an algebraic number. Let z be a nonzero algebraic number of degree d in a field of characteristic zero and w a complex conjugate of z. Then den(z) ^ d * house(z) ^ (d - 1) * ‖w‖ ≥ 1.

theorem TauCeti.one_le_natDenominator_pow_mul_house_pow_mul_norm {z : ℂ} (hz : IsAlgebraic ℚ z) (hz0 : z ≠ 0) : 1 ≤ ↑(Algebra.natDenominator z) ^ (minpoly ℚ z).natDegree * house z ^ ((minpoly ℚ z).natDegree - 1) * ‖z‖

Evertse's lower bound. A nonzero algebraic number z ∈ ℂ of degree d satisfies den(z) ^ d * house(z) ^ (d - 1) * ‖z‖ ≥ 1.

theorem TauCeti.zpow_natDenominator_mul_zpow_house_le_norm {z : ℂ} (hz : IsAlgebraic ℚ z) (hz0 : z ≠ 0) : ↑(Algebra.natDenominator z) ^ (-↑(minpoly ℚ z).natDegree) * house z ^ (1 - ↑(minpoly ℚ z).natDegree) ≤ ‖z‖

The lower bound for a nonzero algebraic number of degree d as an inequality between negative and positive integer powers: den(z) ^ (-d) * house(z) ^ (1 - d) ≤ ‖z‖.

theorem TauCeti.one_le_house_pow_mul_norm_of_mem_rootSet {K : Type u_1} [Field K] [CharZero K] {z : K} {w : ℂ} (hz : IsIntegral ℤ z) (hz0 : z ≠ 0) (hw : w ∈ (minpoly ℚ z).rootSet ℂ) : 1 ≤ house z ^ ((minpoly ℚ z).natDegree - 1) * ‖w‖

The bound for algebraic integers. A nonzero algebraic integer z of degree d in a field of characteristic zero satisfies house(z) ^ (d - 1) * ‖w‖ ≥ 1 for every complex conjugate w of z: its denominator is 1.

theorem TauCeti.one_le_house_pow_mul_norm {z : ℂ} (hz : IsIntegral ℤ z) (hz0 : z ≠ 0) : 1 ≤ house z ^ ((minpoly ℚ z).natDegree - 1) * ‖z‖

The bound for algebraic integers. A nonzero algebraic integer z ∈ ℂ of degree d satisfies house(z) ^ (d - 1) * ‖z‖ ≥ 1: its denominator is 1.

Examples