Projective coefficient heights of univariate polynomials

The height of a polynomial is the native projective height of its coefficient vector. It is unchanged by nonzero scalar multiplication; constants and the zero polynomial have multiplicative height one. The normalization is relative to the admissible family of absolute values on the coefficient field, rather than its degree-root normalization.

The product estimate uses Mathlib's Height.mulHeight_linearMap_apply_le on coefficient convolution. Its archimedean factor counts the coefficients of the smaller-degree factor; the nonarchimedean estimate has no such factor. These estimates are used to control coefficients of auxiliary polynomials in Diophantine approximation.

References

• Lukas Pottmeyer, Diophantine Approximation, §3.2, Definition 3.2.1 and Lemma 3.2.2 (17 January 2022). Those notes use absolute heights; here we use the relative height supplied by Height.AdmissibleAbsValues.

noncomputable def Polynomial.mulHeight {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] (p : Polynomial K) : ℝ

The relative projective multiplicative height of the coefficients of a polynomial.

noncomputable def Polynomial.logHeight {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] (p : Polynomial K) : ℝ

The relative projective logarithmic height of the coefficients of a polynomial.

theorem Polynomial.mulHeight_eq_finsupp {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] (p : Polynomial K) : p.mulHeight = p.toFinsupp.coeff.mulHeight

theorem Polynomial.logHeight_eq_log_mulHeight {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] (p : Polynomial K) : p.logHeight = Real.log p.mulHeight

theorem Polynomial.logHeight_eq_finsupp {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] (p : Polynomial K) : p.logHeight = p.toFinsupp.coeff.logHeight

Polynomial logarithmic height agrees with the native finitely supported height.

theorem Polynomial.mulHeight_eq_support {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] (p : Polynomial K) : p.mulHeight = Height.mulHeight fun (i : ↥p.support) => p.coeff ↑i

Polynomial height is the height of the tuple indexed by its nonzero coefficients.

theorem Polynomial.mulHeight_eq_coeff {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] (p : Polynomial K) {n : ℕ} (hn : p.support ⊆ Finset.range n) : p.mulHeight = Height.mulHeight fun (i : Fin n) => p.coeff ↑i

Any finite coefficient tuple containing the support gives the polynomial height.

theorem Polynomial.logHeight_eq_coeff {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] (p : Polynomial K) {n : ℕ} (hn : p.support ⊆ Finset.range n) : p.logHeight = Height.logHeight fun (i : Fin n) => p.coeff ↑i

The finite coefficient-tuple description of logarithmic polynomial height.

theorem Polynomial.mulHeight_eq_coeff_of_natDegree_lt {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] (p : Polynomial K) {n : ℕ} (hn : p.natDegree < n) : p.mulHeight = Height.mulHeight fun (i : Fin n) => p.coeff ↑i

Any finite coefficient tuple extending past the degree gives the polynomial height.

theorem Polynomial.logHeight_eq_coeff_of_natDegree_lt {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] (p : Polynomial K) {n : ℕ} (hn : p.natDegree < n) : p.logHeight = Height.logHeight fun (i : Fin n) => p.coeff ↑i

The logarithmic coefficient-tuple description when the tuple extends past the degree.

theorem Polynomial.one_le_mulHeight {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] (p : Polynomial K) : 1 ≤ p.mulHeight

theorem Polynomial.mulHeight_pos {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] (p : Polynomial K) : 0 < p.mulHeight

theorem Polynomial.logHeight_nonneg {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] (p : Polynomial K) : 0 ≤ p.logHeight

@[simp]

theorem Polynomial.mulHeight_zero {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] : mulHeight 0 = 1

@[simp]

theorem Polynomial.logHeight_zero {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] : logHeight 0 = 0

@[simp]

theorem Polynomial.mulHeight_monomial {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] (n : ℕ) (c : K) : ((monomial n) c).mulHeight = 1

@[simp]

theorem Polynomial.logHeight_monomial {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] (n : ℕ) (c : K) : ((monomial n) c).logHeight = 0

@[simp]

theorem Polynomial.mulHeight_C {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] (c : K) : (C c).mulHeight = 1

@[simp]

theorem Polynomial.logHeight_C {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] (c : K) : (C c).logHeight = 0

@[simp]

theorem Polynomial.mulHeight_one {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] : mulHeight 1 = 1

@[simp]

theorem Polynomial.logHeight_one {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] : logHeight 1 = 0

@[simp]

theorem Polynomial.mulHeight_X_pow {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] (n : ℕ) : (X ^ n).mulHeight = 1

@[simp]

theorem Polynomial.logHeight_X_pow {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] (n : ℕ) : (X ^ n).logHeight = 0

@[simp]

theorem Polynomial.mulHeight_X {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] : X.mulHeight = 1

@[simp]

theorem Polynomial.logHeight_X {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] : X.logHeight = 0

@[simp]

theorem Polynomial.mulHeight_smul {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] (p : Polynomial K) {c : K} (hc : c ≠ 0) : (c • p).mulHeight = p.mulHeight

Nonzero scalar multiplication does not change projective coefficient height.

@[simp]

theorem Polynomial.mulHeight_C_mul {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] (p : Polynomial K) {c : K} (hc : c ≠ 0) : (C c * p).mulHeight = p.mulHeight

@[simp]

theorem Polynomial.logHeight_smul {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] (p : Polynomial K) {c : K} (hc : c ≠ 0) : (c • p).logHeight = p.logHeight

@[simp]

theorem Polynomial.mulHeight_neg {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] (p : Polynomial K) : (-p).mulHeight = p.mulHeight

@[simp]

theorem Polynomial.logHeight_neg {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] (p : Polynomial K) : (-p).logHeight = p.logHeight

@[simp]

theorem Polynomial.logHeight_C_mul {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] (p : Polynomial K) {c : K} (hc : c ≠ 0) : (C c * p).logHeight = p.logHeight

@[simp]

theorem Polynomial.mulHeight_X_sub_C {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] (a : K) : (X - C a).mulHeight = Height.mulHeight₁ a

The coefficient height of the linear polynomial with root a is the scalar height of a.

@[simp]

theorem Polynomial.logHeight_X_sub_C {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] (a : K) : (X - C a).logHeight = Height.logHeight₁ a

The logarithmic coefficient height of the linear polynomial with root a is the scalar logarithmic height of a.

theorem Polynomial.mulHeight_mul_le {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] (f g : Polynomial K) : (f * g).mulHeight ≤ ↑(min f.natDegree g.natDegree + 1) ^ Height.totalWeight K * f.mulHeight * g.mulHeight

The height of a product is bounded by the product of coefficient heights, with the archimedean convolution factor given by the smaller degree plus one.

theorem Polynomial.logHeight_mul_le {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] (f g : Polynomial K) : (f * g).logHeight ≤ ↑(Height.totalWeight K) * Real.log ↑(min f.natDegree g.natDegree + 1) + f.logHeight + g.logHeight

The logarithmic form of the coefficient convolution estimate.