Heights of integer tuples and integer polynomials over ℚ

Mathlib's Rat.mulHeight_eq_max_abs_of_gcd_eq_one computes the height over ℚ of a tuple of coprime integers as the largest absolute value of its entries. Every finite place contributes at most 1 to the height of an integer tuple, so for an arbitrary nonzero integer tuple the largest absolute value is still an upper bound for the height:

H(x) ≤ maxᵢ |xᵢ|, with equality if gcd(x) = 1.

The same holds for finitely supported integer vectors, and hence for the coefficient heights of integer polynomials viewed over ℚ: for every P ∈ ℤ[X₁, …, Xₙ], h(P) ≤ log maxμ |Pμ|, with equality if the coefficients of P are coprime.

This is how an integer auxiliary polynomial with coefficients bounded by B, such as the one of TauCeti.exists_roth_auxiliary_polynomial, gets the height bound h(P) ≤ log B required by height estimates such as Roth's lemma.

Main results

• Rat.mulHeight_le_max_abs: H(x) ≤ maxᵢ |xᵢ| for a nonzero integer tuple x.
• Rat.den_le_mulHeight₁, Rat.log_den_le_logHeight₁: the denominator of a rational number is at most its height.
• Rat.mulHeight₁_le_max_one_abs_mul_den: conversely, H(q) ≤ max(1, |q|) den(q).
• Rat.mulHeight₁_intCast_div_le: H(x / y) ≤ max(|x|, |y|) for integers x and y ≠ 0, with equality for coprime x and y (Rat.mulHeight₁_intCast_div_of_isCoprime).
• MvPolynomial.IsHomogeneous.max_abs_le_abs_eval_rpow_mul_mulHeight₁: conversely, if F is an integer binary form of degree n ≠ 0 with F(x, y) ≠ 0, then max(|x|, |y|) ≤ |F(x, y)| ^ (1 / n) H(x / y).
• Rat.abs_padicValRat_mul_log_le_logHeight₁, Rat.abs_padicValRat_le_logHeight₁_div_log_two: the p-adic valuation of a rational number is bounded by its logarithmic height, |v_p(q)| log p ≤ h(q), and hence |v_p(q)| ≤ h(q) / log 2.
• Finsupp.mulHeight_mapRange_intCast_le, Finsupp.mulHeight_mapRange_intCast_eq: the bound, and the equality for coprime entries, for finitely supported integer vectors.
• Finsupp.mulHeight_mapRange_intCast_le_of_abs_le: H(x) ≤ B if all entries of the nonzero integer vector x are bounded by B in absolute value.
• MvPolynomial.logHeight_map_intCast_le, MvPolynomial.logHeight_map_intCast_eq: for an integer polynomial, h(P) ≤ log maxμ |Pμ|, with equality for coprime coefficients.
• MvPolynomial.logHeight_map_intCast_le_log: h(P) ≤ log B if all coefficients of the nonzero integer polynomial P are bounded by B in absolute value.
• Polynomial.logHeight_map_intCast_le, Polynomial.logHeight_map_intCast_eq, Polynomial.logHeight_map_intCast_le_log: the same for univariate polynomials, where coprime coefficients means that P is primitive.

References

• L. Pottmeyer, Diophantine Approximation (2022), §3.5.2.

theorem Rat.mulHeight_le_max_abs {ι : Type u_1} [Finite ι] {x : ι → ℤ} (hx : x ≠ 0) : Height.mulHeight (Int.cast ∘ x) ≤ ↑(⨆ (i : ι), |x i|)

The height of a nonzero tuple of integers, viewed as rational numbers, is at most the largest absolute value of its entries. Equality holds for coprime entries, by Rat.mulHeight_eq_max_abs_of_gcd_eq_one.

theorem Rat.logHeight_le_max_abs {ι : Type u_1} [Finite ι] (x : ι → ℤ) : Height.logHeight (Int.cast ∘ x) ≤ Real.log ↑(⨆ (i : ι), |x i|)

The logarithmic height of a tuple of integers, viewed as rational numbers, is at most the logarithm of the largest absolute value of its entries.

theorem Rat.den_le_mulHeight₁ (q : ℚ) : ↑q.den ≤ Height.mulHeight₁ q

The denominator of a rational number is at most its multiplicative height.

theorem Rat.mulHeight₁_le_max_one_abs_mul_den (q : ℚ) : Height.mulHeight₁ q ≤ max 1 |↑q| * ↑q.den

The multiplicative height of a rational number q is at most max 1 |q| times its denominator.

theorem Rat.mulHeight₁_intCast_div_le (x : ℤ) {y : ℤ} (hy : y ≠ 0) : Height.mulHeight₁ (↑x / ↑y) ≤ max |↑x| |↑y|

The multiplicative height of a quotient x / y of integers with y ≠ 0 is at most max(|x|, |y|).

theorem Rat.mulHeight₁_intCast_div_of_isCoprime {x y : ℤ} (h : IsCoprime x y) : Height.mulHeight₁ (↑x / ↑y) = max |↑x| |↑y|

The multiplicative height of a quotient x / y of coprime integers is max(|x|, |y|). This includes y = 0, where x = ±1 and x / y = 0 has height 1.

theorem Rat.log_den_le_logHeight₁ (q : ℚ) : Real.log ↑q.den ≤ Height.logHeight₁ q

The logarithm of the denominator of a rational number is at most its logarithmic height.

theorem Rat.abs_padicValRat_mul_log_le_logHeight₁ (p : ℕ) (q : ℚ) : |↑(padicValRat p q)| * Real.log ↑p ≤ Height.logHeight₁ q

The p-adic valuation of a rational number is bounded by its logarithmic height: |v_p(q)| log p ≤ h(q).

theorem Rat.abs_padicValRat_le_logHeight₁_div_log_two (p : ℕ) (q : ℚ) : |↑(padicValRat p q)| ≤ Height.logHeight₁ q / Real.log 2

The p-adic valuation of a rational number is bounded by its logarithmic height: |v_p(q)| ≤ h(q) / log 2.

theorem Finsupp.mulHeight_mapRange_intCast_le {α : Type u_1} {x : α →₀ ℤ} (hx : x ≠ 0) : (mapRange Int.cast ⋯ x).mulHeight ≤ ↑(x.support.sup fun (a : α) => (x a).natAbs)

The height over ℚ of a nonzero finitely supported integer vector is at most the largest absolute value of its entries.

theorem Finsupp.mulHeight_mapRange_intCast_le_of_abs_le {α : Type u_1} {x : α →₀ ℤ} (hx : x ≠ 0) {B : ℝ} (hB : ∀ (a : α), |↑(x a)| ≤ B) : (mapRange Int.cast ⋯ x).mulHeight ≤ B

If the entries of a nonzero finitely supported integer vector are bounded by B in absolute value, then its height over ℚ is at most B.

theorem Finsupp.mulHeight_mapRange_intCast_eq {α : Type u_1} {x : α →₀ ℤ} (hx : x.support.gcd ⇑x = 1) : (mapRange Int.cast ⋯ x).mulHeight = ↑(x.support.sup fun (a : α) => (x a).natAbs)

The height over ℚ of a finitely supported integer vector with coprime entries is the largest absolute value of its entries.

theorem MvPolynomial.mulHeight_map_intCast_le {σ : Type u_1} {P : MvPolynomial σ ℤ} (hP : P ≠ 0) : ((map (Int.castRingHom ℚ)) P).mulHeight ≤ ↑(P.support.sup fun (m : σ →₀ ℕ) => (P.coeff m).natAbs)

The height over ℚ of a nonzero integer polynomial is at most the largest absolute value of its coefficients.

theorem MvPolynomial.mulHeight_map_intCast_eq {σ : Type u_1} {P : MvPolynomial σ ℤ} (hP : P.support.gcd ⇑P.coeff = 1) : ((map (Int.castRingHom ℚ)) P).mulHeight = ↑(P.support.sup fun (m : σ →₀ ℕ) => (P.coeff m).natAbs)

The height over ℚ of an integer polynomial with coprime coefficients is the largest absolute value of its coefficients.

theorem MvPolynomial.logHeight_map_intCast_le {σ : Type u_1} (P : MvPolynomial σ ℤ) : ((map (Int.castRingHom ℚ)) P).logHeight ≤ Real.log ↑(P.support.sup fun (m : σ →₀ ℕ) => (P.coeff m).natAbs)

Pottmeyer, §3.5.2. The logarithmic height over ℚ of an integer polynomial is at most the logarithm of the largest absolute value of its coefficients.

theorem MvPolynomial.logHeight_map_intCast_eq {σ : Type u_1} {P : MvPolynomial σ ℤ} (hP : P.support.gcd ⇑P.coeff = 1) : ((map (Int.castRingHom ℚ)) P).logHeight = Real.log ↑(P.support.sup fun (m : σ →₀ ℕ) => (P.coeff m).natAbs)

The logarithmic height over ℚ of an integer polynomial with coprime coefficients is the logarithm of the largest absolute value of its coefficients.

theorem MvPolynomial.logHeight_map_intCast_le_log {σ : Type u_1} {P : MvPolynomial σ ℤ} (hP : P ≠ 0) {B : ℝ} (hB : ∀ (m : σ →₀ ℕ), |↑(P.coeff m)| ≤ B) : ((map (Int.castRingHom ℚ)) P).logHeight ≤ Real.log B

If the coefficients of a nonzero integer polynomial P are bounded by B in absolute value, then the logarithmic height of P over ℚ is at most log B.

theorem Polynomial.mulHeight_map_intCast_le {P : Polynomial ℤ} (hP : P ≠ 0) : (map (Int.castRingHom ℚ) P).mulHeight ≤ ↑(P.support.sup fun (n : ℕ) => (P.coeff n).natAbs)

The height over ℚ of a nonzero integer polynomial is at most the largest absolute value of its coefficients.

theorem Polynomial.mulHeight_map_intCast_eq {P : Polynomial ℤ} (hP : P.IsPrimitive) : (map (Int.castRingHom ℚ) P).mulHeight = ↑(P.support.sup fun (n : ℕ) => (P.coeff n).natAbs)

The height over ℚ of a primitive integer polynomial is the largest absolute value of its coefficients.

theorem Polynomial.logHeight_map_intCast_le (P : Polynomial ℤ) : (map (Int.castRingHom ℚ) P).logHeight ≤ Real.log ↑(P.support.sup fun (n : ℕ) => (P.coeff n).natAbs)

The logarithmic height over ℚ of an integer polynomial is at most the logarithm of the largest absolute value of its coefficients.

theorem Polynomial.logHeight_map_intCast_eq {P : Polynomial ℤ} (hP : P.IsPrimitive) : (map (Int.castRingHom ℚ) P).logHeight = Real.log ↑(P.support.sup fun (n : ℕ) => (P.coeff n).natAbs)

The logarithmic height over ℚ of a primitive integer polynomial is the logarithm of the largest absolute value of its coefficients.

theorem Polynomial.logHeight_map_intCast_le_log {P : Polynomial ℤ} (hP : P ≠ 0) {B : ℝ} (hB : ∀ (n : ℕ), |↑(P.coeff n)| ≤ B) : (map (Int.castRingHom ℚ) P).logHeight ≤ Real.log B

If the coefficients of a nonzero integer polynomial P are bounded by B in absolute value, then the logarithmic height of P over ℚ is at most log B.

theorem MvPolynomial.IsHomogeneous.max_abs_le_abs_eval_rpow_mul_mulHeight₁ {F : MvPolynomial (Fin 2) ℤ} {n : ℕ} (hF : F.IsHomogeneous n) (hn : n ≠ 0) {x y : ℤ} (h : (eval ![x, y]) F ≠ 0) : max |↑x| |↑y| ≤ |↑((eval ![x, y]) F)| ^ (1 / ↑n) * Height.mulHeight₁ (↑x / ↑y)

The size of an integer point from the height of its ratio. Let F be a binary form of degree n ≠ 0 with integer coefficients and let x, y be integers with F(x, y) ≠ 0. Then max(|x|, |y|) ≤ |F(x, y)| ^ (1 / n) H(x / y). In particular a height bound for the ratios x / y of the solutions of a Thue equation F(x, y) = m bounds the solutions themselves.