Mahler's exponent: Liouville's bound and Möbius invariance #

Let ξ be an algebraic number of degree D over ℚ. A nonzero value of an integer polynomial P of degree at most n at ξ cannot be too small: there is c > 0, depending only on ξ and n, with |P(ξ)| ≥ c H(P) ^ (-(D - 1)), where H(P) is the largest absolute value of a coefficient of P. Consequently Mahler's exponent satisfies wₙ(ξ) ≤ D - 1 for every n.

The exponent is D - 1 and not D. If a is the leading coefficient of the primitive minimal polynomial of ξ, then γ = (P.scaleRoots a)(a ξ) = a ^ (deg P) P(ξ) is a nonzero algebraic integer of ℚ(ξ), so the product of its D conjugates, its norm, is a nonzero integer. The conjugate at ξ itself is a ^ (deg P) P(ξ), and only the other D - 1 conjugates are bounded above in terms of H(P).

Mahler's exponent is also invariant under rational Möbius transformations ξ ↦ (a ξ + b) / (c ξ + d) with a d - b c ≠ 0, like the irrationality exponent (TauCeti.irrationalityExponent_mul_add_div_mul_add). After clearing denominators the coefficients are integers, and an integer polynomial P of degree at most n goes to the integer polynomial (c X + d) ^ n P((a X + b) / (c X + d)) of degree at most n, obtained by substituting a X + b and c X + d into the homogenization of P. Its value at ξ is (c ξ + d) ^ n times the value of P at the image of ξ, and its coefficients are bounded by a constant times those of P, so the approximations transfer (TauCeti.linearFormExponent_le_of_map). The inverse transformation gives the reverse inequality.

Main results #

IsAlgebraic.exists_pos_le_norm_aeval_mul_supNorm_pow: Liouville's inequality for the value of an integer polynomial, c ≤ |P(ξ)| H(P) ^ (D - 1) for complex algebraic ξ and P ∈ ℤ[X] of degree at most n with P(ξ) ≠ 0.
IsAlgebraic.mahlerExponent_le: for real algebraic ξ of degree D, wₙ(ξ) ≤ D - 1.
TauCeti.mahlerExponent_eq_of_natDegree_minpoly_eq: for real ξ algebraic of degree n + 1, wₙ(ξ) = n, so the bound is attained.
TauCeti.mahlerExponent_ratCast: rational numbers have Mahler exponent 0 in every degree.
TauCeti.mahlerExponent_mul_add_div_mul_add: wₙ is invariant under rational Möbius transformations of nonzero determinant; in particular under adding or multiplying by a nonzero rational number, negation and inversion (TauCeti.mahlerExponent_add_ratCast, TauCeti.mahlerExponent_ratCast_mul, TauCeti.mahlerExponent_neg, TauCeti.mahlerExponent_inv).

References #

Y. Bugeaud, Approximation by Algebraic Numbers, Cambridge Tracts in Mathematics 160, 2004, Chapter 3.

source

theorem IsAlgebraic.exists_pos_le_norm_aeval_mul_supNorm_pow {ξ : ℂ} (hξ : IsAlgebraic ℚ ξ) (n : ℕ) :

∃ c > 0, ∀ (P : Polynomial ℤ), P.natDegree ≤ n → (Polynomial.aeval ξ) P ≠ 0 → c ≤ ‖(Polynomial.aeval ξ) P‖ * P.supNorm ^ ((minpoly ℚ ξ).natDegree - 1)

Liouville's inequality for the value of an integer polynomial. Let ξ ∈ ℂ be algebraic of degree D over ℚ and let n ∈ ℕ. There is c > 0 such that every P ∈ ℤ[X] of degree at most n with P(ξ) ≠ 0 satisfies c ≤ |P(ξ)| H(P) ^ (D - 1), where H(P) is the coefficient sup norm of P.

source

theorem IsAlgebraic.mahlerExponent_le {ξ : ℝ} (hξ : IsAlgebraic ℚ ξ) (n : ℕ) :

TauCeti.mahlerExponent n ξ ≤ ↑((minpoly ℚ ξ).natDegree - 1)

Liouville's bound for Mahler's exponent. If ξ is a real algebraic number of degree D over ℚ, then wₙ(ξ) ≤ D - 1 for every n.

source

theorem TauCeti.mahlerExponent_eq_of_natDegree_minpoly_eq {ξ : ℝ} {n : ℕ} (hn : (minpoly ℚ ξ).natDegree = n + 1) :

mahlerExponent n ξ = ↑n

For a real algebraic number ξ of degree n + 1 over ℚ, Mahler's exponent in degree n is exactly n, so Liouville's bound wₙ(ξ) ≤ D - 1 is attained for D = n + 1. For instance, w₁(ξ) = 1 for every real quadratic irrational ξ.

source

@[simp]

theorem TauCeti.mahlerExponent_ratCast (n : ℕ) (q : ℚ) :

mahlerExponent n ↑q = 0

Rational numbers have Mahler exponent 0 in every degree.

Invariance under rational Möbius transformations #

source

theorem TauCeti.mahlerExponent_mul_add_div_mul_add (n : ℕ) (ξ : ℝ) {a b c d : ℚ} (h : a * d - b * c ≠ 0) :

mahlerExponent n ((↑a * ξ + ↑b) / (↑c * ξ + ↑d)) = mahlerExponent n ξ

Mahler's exponent wₙ is invariant under a Möbius transformation ξ ↦ (a ξ + b) / (c ξ + d) with rational coefficients and nonzero determinant a d - b c. At the pole ξ = -d / c, where Lean's convention x / 0 = 0 applies, both sides vanish because both points are rational.

source

@[simp]