Liouville's inequality with an explicit constant

Let f ∈ ℤ[X] have degree d and a complex root α, and let ξ = p / q be a rational number, written in lowest terms with q > 0, at which f does not vanish. The value of the homogenization of f at (p, q) is the nonzero integer q ^ d f(ξ), so it has absolute value at least 1. Comparing with the upper bound of Polynomial.norm_eval_homogenize_le_mahlerMeasure_mul_norm_div_sub gives Liouville's inequality |ξ - α| ≥ (2 ^ (d - 1) M(f) H(ξ) ^ d)⁻¹, where M(f) is the Mahler measure of f and H(ξ) = max(|p|, q) is the height of ξ.

For an algebraic number α we apply this to its primitive minimal polynomial F_α, which vanishes at no rational number other than α.

Main results

• Polynomial.inv_le_norm_ratCast_sub: Liouville's inequality for an integer polynomial f with root α at a rational ξ with f(ξ) ≠ 0.
• IsAlgebraic.inv_le_norm_ratCast_sub: Liouville's inequality for an algebraic number α of degree d and a rational number ξ ≠ α, with constant 2 ^ (1 - d) M(F_α)⁻¹.

References

• J.-H. Evertse, Diophantine Approximation, lecture notes (2019), ch. 6, Theorem 6.1.

theorem Polynomial.inv_le_norm_ratCast_sub (f : Polynomial ℤ) {α : ℂ} (hα : (map (Int.castRingHom ℂ) f).IsRoot α) {ξ : ℚ} (hξ : (aeval ξ) f ≠ 0) : (2 ^ (f.natDegree - 1) * (map (Int.castRingHom ℂ) f).mahlerMeasure * Height.mulHeight₁ ξ ^ f.natDegree)⁻¹ ≤ ‖↑ξ - α‖

Liouville's inequality. Let f ∈ ℤ[X] have degree d and a complex root α. Every rational number ξ with f(ξ) ≠ 0 satisfies |ξ - α| ≥ (2 ^ (d - 1) M(f) H(ξ) ^ d)⁻¹, where M(f) is the Mahler measure of f and H(ξ) the height of ξ.

theorem IsAlgebraic.inv_le_norm_ratCast_sub {α : ℂ} (hα : IsAlgebraic ℚ α) {ξ : ℚ} (hξ : ↑ξ ≠ α) : (2 ^ ((minpoly ℚ α).natDegree - 1) * (Polynomial.map (Int.castRingHom ℂ) (TauCeti.primitiveMinpoly α)).mahlerMeasure * Height.mulHeight₁ ξ ^ (minpoly ℚ α).natDegree)⁻¹ ≤ ‖↑ξ - α‖

Liouville's inequality for an algebraic number. Let α ∈ ℂ be algebraic of degree d with primitive minimal polynomial F_α ∈ ℤ[X]. Every rational number ξ ≠ α satisfies |ξ - α| ≥ (2 ^ (d - 1) M(F_α) H(ξ) ^ d)⁻¹, where M(F_α) is the Mahler measure of F_α (the Mahler measure of α) and H(ξ) the height of ξ.