Basic coefficient sup-norm estimates

Reversal and norm-preserving maps of coefficients preserve the coefficient sup norm. Multiplication by a constant scales it when the coefficient norm is multiplicative.

A coefficient of a finite product is bounded by its binomial weight in the sum of the degrees times the product of the coefficient sup norms. Consequently the sup norm of the product is bounded by the middle binomial coefficient. Over a domain this gives a factor of at most 2 ^ d, where d is the degree of the product.

These estimates control growth of coefficients under polynomial multiplication. They include zero factors and empty products, and use Mathlib's Polynomial.supNorm.

References

• Xiaorun Wu, Diophantine geometry, week 08: arithmetic heights (2023), Lemma 3.6.

@[simp]

theorem Polynomial.supNorm_map {R : Type u_1} {S : Type u_2} [SeminormedRing R] [SeminormedRing S] (p : Polynomial R) (f : R →+* S) [RingHomIsometric f] : (map f p).supNorm = p.supNorm

A norm-preserving ring homomorphism preserves the coefficient sup norm.

@[simp]

theorem Polynomial.supNorm_reverse {R : Type u_1} [SeminormedRing R] (p : Polynomial R) : p.reverse.supNorm = p.supNorm

Reversing a polynomial preserves its coefficient sup norm.

theorem Polynomial.norm_coeff_le_choose_mul_supNorm {A : Type u_1} [SeminormedRing A] (p : Polynomial A) (k : ℕ) : ‖p.coeff k‖ ≤ ↑(p.natDegree.choose k) * p.supNorm

A coefficient is bounded by its binomial weight times the coefficient sup norm.

theorem Polynomial.norm_coeff_prod_le_choose_mul_prod_supNorm {A : Type u_1} {ι : Type u_2} [SeminormedCommRing A] [NormOneClass A] (s : Finset ι) (f : ι → Polynomial A) (k : ℕ) : ‖(∏ i ∈ s, f i).coeff k‖ ≤ ↑((∑ i ∈ s, (f i).natDegree).choose k) * ∏ i ∈ s, (f i).supNorm

Each coefficient of a finite product is bounded by a binomial coefficient of the sum of the degrees times the product of the coefficient sup norms.

theorem Polynomial.supNorm_prod_le_choose_mul_prod_supNorm {A : Type u_1} {ι : Type u_2} [SeminormedCommRing A] [NormOneClass A] (s : Finset ι) (f : ι → Polynomial A) : (∏ i ∈ s, f i).supNorm ≤ ↑((∑ i ∈ s, (f i).natDegree).choose ((∑ i ∈ s, (f i).natDegree) / 2)) * ∏ i ∈ s, (f i).supNorm

The coefficient sup norm of a finite product is at most the largest binomial coefficient of the sum of the degrees times the product of the sup norms.

theorem Polynomial.supNorm_prod_le_two_pow_mul_prod_supNorm {A : Type u_1} {ι : Type u_2} [SeminormedCommRing A] [NormOneClass A] [IsDomain A] (s : Finset ι) (f : ι → Polynomial A) : (∏ i ∈ s, f i).supNorm ≤ 2 ^ (∏ i ∈ s, f i).natDegree * ∏ i ∈ s, (f i).supNorm

The coefficient sup norm of a product of polynomials over a seminormed commutative domain is at most 2^d times the product of the coefficient sup norms, where d is the degree of the product.

@[simp]

theorem Polynomial.supNorm_mul_C {A : Type u_1} [SeminormedRing A] [NormMulClass A] (p : Polynomial A) (a : A) : (p * C a).supNorm = p.supNorm * ‖a‖

Multiplication by a constant scales the coefficient sup norm when the coefficient norm is multiplicative.