Absolute values of values of polynomials

Let P be a polynomial over a commutative ring R with partial degrees degreeOf i P ≤ L i and coefficients of absolute value at most B under an absolute value v on R. Then P(x) is a sum of at most ∏ i, (L i + 1) terms, each at most B ∏ i, max(v(x_i), 1) ^ L i, so

• v(P(x)) ≤ B ∏ i, (L i + 1) ∏ i, max(v(x_i), 1) ^ L i;
• if v is nonarchimedean, the ultrametric inequality removes the count: v(P(x)) ≤ B ∏ i, max(v(x_i), 1) ^ L i.

For an integer polynomial P ∈ ℤ[X_i : i ∈ ι] with length ℓ(P) = ∑_s |c_s|, the sum of the absolute values of its coefficients, the value at a point x of R satisfies:

• v(P(x)) ≤ ℓ(P) ∏ i, max(v(x_i), 1) ^ L i;
• if v is nonarchimedean, the integer coefficients have v(c_s) ≤ 1, so v(P(x)) ≤ ∏ i, max(v(x_i), 1) ^ L i.

These are the local estimates behind height bounds for values of polynomials.

Main results

• MvPolynomial.one_le_sum_abs_coeff: a nonzero integer polynomial has length ℓ(P) ≥ 1.
• AbsoluteValue.apply_prod_pow_le: v(∏ i, x_i ^ s_i) ≤ ∏ i, max(v(x_i), 1) ^ L i for s ≤ L.
• AbsoluteValue.apply_coeff_mul_prod_pow_le: the same bound v(c_s) ∏ i, max(v(x_i), 1) ^ L i for a single term c_s ∏ i, x_i ^ s_i of P(x).
• AbsoluteValue.apply_eval_le, IsNonarchimedean.apply_eval_le: the bounds for a polynomial over R with coefficients of absolute value at most B.
• AbsoluteValue.apply_aeval_le: v(P(x)) ≤ ℓ(P) ∏ i, max(v(x_i), 1) ^ L i.
• IsNonarchimedean.apply_aeval_le: v(P(x)) ≤ ∏ i, max(v(x_i), 1) ^ L i for nonarchimedean v.

References

• E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), §1.6.

theorem MvPolynomial.one_le_sum_abs_coeff {ι : Type u_1} {P : MvPolynomial ι ℤ} (hP : P ≠ 0) : 1 ≤ ∑ s ∈ P.support, |↑(P.coeff s)|

A nonzero integer polynomial has length ℓ(P) ≥ 1: the sum of the absolute values of its coefficients is at least 1, since it has a nonzero integer coefficient.

theorem AbsoluteValue.apply_prod_pow_le {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] (v : AbsoluteValue R ℝ) {s L : ι → ℕ} (hs : ∀ (i : ι), s i ≤ L i) (x : ι → R) : v (∏ i : ι, x i ^ s i) ≤ ∏ i : ι, max (v (x i)) 1 ^ L i

A monomial ∏ i, x_i ^ s_i with exponents s_i ≤ L i has absolute value at most ∏ i, max(v(x_i), 1) ^ L i.

theorem AbsoluteValue.apply_coeff_mul_prod_pow_le {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] (v : AbsoluteValue R ℝ) {P : MvPolynomial ι ℤ} {L : ι → ℕ} (hL : ∀ (i : ι), MvPolynomial.degreeOf i P ≤ L i) (x : ι → R) {s : ι →₀ ℕ} (hs : s ∈ P.support) : v ((algebraMap ℤ R) (P.coeff s) * ∏ i : ι, x i ^ s i) ≤ v ↑(P.coeff s) * ∏ i : ι, max (v (x i)) 1 ^ L i

A term c_s ∏ i, x_i ^ s_i of the value at x of an integer polynomial P with partial degrees degreeOf i P ≤ L i has absolute value at most v(c_s) ∏ i, max(v(x_i), 1) ^ L i.

theorem AbsoluteValue.apply_aeval_le {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] (v : AbsoluteValue R ℝ) {P : MvPolynomial ι ℤ} {L : ι → ℕ} (hL : ∀ (i : ι), MvPolynomial.degreeOf i P ≤ L i) (x : ι → R) : v ((MvPolynomial.aeval x) P) ≤ (∑ s ∈ P.support, |↑(P.coeff s)|) * ∏ i : ι, max (v (x i)) 1 ^ L i

The value of an integer polynomial P with partial degrees degreeOf i P ≤ L i at a point x has absolute value at most ℓ(P) ∏ i, max(v(x_i), 1) ^ L i, where ℓ(P) is the sum of the absolute values of the coefficients of P.

theorem AbsoluteValue.apply_eval_le {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] (v : AbsoluteValue R ℝ) {P : MvPolynomial ι R} {L : ι → ℕ} (hL : ∀ (i : ι), MvPolynomial.degreeOf i P ≤ L i) {B : ℝ} (hB : ∀ (s : ι →₀ ℕ), v (P.coeff s) ≤ B) (x : ι → R) : v ((MvPolynomial.eval x) P) ≤ (B * ∏ i : ι, (↑(L i) + 1)) * ∏ i : ι, max (v (x i)) 1 ^ L i

The trivial bound for the value of a polynomial. If P has partial degrees degreeOf i P ≤ L i and coefficients of absolute value at most B, then v(P(x)) ≤ B ∏ i, (L i + 1) ∏ i, max(v(x_i), 1) ^ L i.

theorem IsNonarchimedean.apply_eval_le {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] {v : AbsoluteValue R ℝ} (hv : IsNonarchimedean ⇑v) {P : MvPolynomial ι R} {L : ι → ℕ} (hL : ∀ (i : ι), MvPolynomial.degreeOf i P ≤ L i) {B : ℝ} (hB : ∀ (s : ι →₀ ℕ), v (P.coeff s) ≤ B) (x : ι → R) : v ((MvPolynomial.eval x) P) ≤ B * ∏ i : ι, max (v (x i)) 1 ^ L i

The trivial bound at a nonarchimedean absolute value. If P has partial degrees degreeOf i P ≤ L i and coefficients of absolute value at most B, then v(P(x)) ≤ B ∏ i, max(v(x_i), 1) ^ L i.

theorem IsNonarchimedean.apply_aeval_le {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] {v : AbsoluteValue R ℝ} (hv : IsNonarchimedean ⇑v) {P : MvPolynomial ι ℤ} {L : ι → ℕ} (hL : ∀ (i : ι), MvPolynomial.degreeOf i P ≤ L i) (x : ι → R) : v ((MvPolynomial.aeval x) P) ≤ ∏ i : ι, max (v (x i)) 1 ^ L i

At a nonarchimedean absolute value the value of an integer polynomial P with partial degrees degreeOf i P ≤ L i at a point x has absolute value at most ∏ i, max(v(x_i), 1) ^ L i: the integer coefficients have absolute value at most 1.