The coefficient l¹-norm of a polynomial

This file defines the coefficient l¹-norm (also called the coefficient length) of a polynomial and develops its basic estimates. In particular, it is subadditive and submultiplicative, controls evaluation, and behaves predictably under translation and Hasse differentiation. These bounds are useful when constructing auxiliary polynomials with controlled coefficients.

Main definitions

• Polynomial.l1Norm: the sum of the norms of the nonzero coefficients.

Main results

• Polynomial.l1Norm_add_le and Polynomial.l1Norm_mul_le: the triangle and product bounds.
• Polynomial.norm_eval_le_l1Norm_mul: the evaluation bound, and Polynomial.norm_eval_le_add_one_mul_supNorm_mul: its form in terms of the sup norm.
• Polynomial.l1Norm_comp_le and Polynomial.l1Norm_comp_X_add_C_le: the composition and translation bounds.
• Polynomial.l1Norm_hasseDeriv_le and Polynomial.l1Norm_hasseDeriv_le_pow: Hasse derivative bounds in terms of the degree and coefficient length.
• Polynomial.l1Norm_mul_X_pow and Polynomial.l1Norm_map: invariance under shifts and norm-preserving coefficient maps.
• Polynomial.norm_eval_le_l1Norm_mul_of_mul_X_sub_C_pow_eq: the values near a of the quotient of a polynomial by a power of X - a.
• Polynomial.l1Norm_aeval_homogenize_le: the bound ‖p‖∞ (‖g‖₁ + ‖h‖₁) ^ n after substituting g and h into the homogenization of degree n of p.

References

• J.-H. Evertse, Diophantine Approximation, Chapter 6, Section 6.2.

noncomputable def Polynomial.l1Norm {R : Type u_1} [SeminormedRing R] (P : Polynomial R) : ℝ

The coefficient l¹-norm of a polynomial, namely the sum of the norms of its nonzero coefficients. This is also called the coefficient length.

theorem Polynomial.l1Norm_eq_sum_support {R : Type u_1} [SeminormedRing R] (P : Polynomial R) : P.l1Norm = ∑ i ∈ P.support, ‖P.coeff i‖

The coefficient l¹-norm is the sum over the support.

theorem Polynomial.l1Norm_eq_sum_of_support_subset {R : Type u_1} [SeminormedRing R] (P : Polynomial R) {s : Finset ℕ} (h : P.support ⊆ s) : P.l1Norm = ∑ i ∈ s, ‖P.coeff i‖

The coefficient l¹-norm is the sum over any finite set containing the support.

theorem Polynomial.l1Norm_eq_sum_range {R : Type u_1} [SeminormedRing R] (P : Polynomial R) : P.l1Norm = ∑ i ∈ Finset.range (P.natDegree + 1), ‖P.coeff i‖

The coefficient l¹-norm is the sum through the natural degree.

theorem Polynomial.sum_support_norm_coeff_mul_le {R : Type u_1} [SeminormedRing R] (P : Polynomial R) (f : ℕ → ℝ) {c : ℝ} (hf : ∀ i ∈ P.support, f i ≤ c) : ∑ i ∈ P.support, ‖P.coeff i‖ * f i ≤ P.l1Norm * c

A sum over the support of coefficient norms weighted by factors bounded by c is at most c times the coefficient l¹-norm.

@[simp]

theorem Polynomial.l1Norm_zero {R : Type u_1} [SeminormedRing R] : l1Norm 0 = 0

The zero polynomial has coefficient l¹-norm zero.

theorem Polynomial.l1Norm_nonneg {R : Type u_1} [SeminormedRing R] (P : Polynomial R) : 0 ≤ P.l1Norm

The coefficient l¹-norm is nonnegative.

@[simp]

theorem Polynomial.l1Norm_C {R : Type u_1} [SeminormedRing R] (a : R) : (C a).l1Norm = ‖a‖

The coefficient l¹-norm of a constant polynomial is the norm of its value.

@[simp]

theorem Polynomial.l1Norm_monomial {R : Type u_1} [SeminormedRing R] (n : ℕ) (a : R) : ((monomial n) a).l1Norm = ‖a‖

The coefficient l¹-norm of a monomial is the norm of its coefficient.

@[simp]

theorem Polynomial.l1Norm_one {R : Type u_1} [SeminormedRing R] [NormOneClass R] : l1Norm 1 = 1

The unit polynomial has coefficient l¹-norm one when the coefficient norm preserves one.

@[simp]

theorem Polynomial.l1Norm_X {R : Type u_1} [SeminormedRing R] [NormOneClass R] : X.l1Norm = 1

The polynomial X has coefficient l¹-norm one when the coefficient norm preserves one.

@[simp]

theorem Polynomial.l1Norm_X_pow {R : Type u_1} [SeminormedRing R] [NormOneClass R] (n : ℕ) : (X ^ n).l1Norm = 1

The powers of X have coefficient l¹-norm one when the coefficient norm preserves one.

@[simp]

theorem Polynomial.l1Norm_neg {R : Type u_1} [SeminormedRing R] (P : Polynomial R) : (-P).l1Norm = P.l1Norm

Negating a polynomial does not change its coefficient l¹-norm.

@[simp]

theorem Polynomial.l1Norm_mul_X_pow {R : Type u_1} [SeminormedRing R] (P : Polynomial R) (n : ℕ) : (P * X ^ n).l1Norm = P.l1Norm

Multiplying by a power of X shifts the coefficients, so it does not change the coefficient l¹-norm.

theorem Polynomial.l1Norm_map {R : Type u_1} [SeminormedRing R] (P : Polynomial R) {S : Type u_2} [SeminormedRing S] (f : R →+* S) (hf : ∀ (x : R), ‖f x‖ = ‖x‖) : (map f P).l1Norm = P.l1Norm

A norm-preserving ring homomorphism preserves the coefficient l¹-norm.

theorem Polynomial.norm_coeff_le_l1Norm {R : Type u_1} [SeminormedRing R] (P : Polynomial R) (i : ℕ) : ‖P.coeff i‖ ≤ P.l1Norm

The norm of each coefficient is at most the coefficient l¹-norm.

theorem Polynomial.supNorm_le_l1Norm {R : Type u_1} [SeminormedRing R] (P : Polynomial R) : P.supNorm ≤ P.l1Norm

The coefficient sup norm is at most the coefficient l¹-norm.

theorem Polynomial.l1Norm_le_natDegree_add_one_mul_supNorm {R : Type u_1} [SeminormedRing R] (P : Polynomial R) : P.l1Norm ≤ (↑P.natDegree + 1) * P.supNorm

The coefficient l¹-norm is at most the number of possible coefficients times the sup norm.

@[simp]

theorem Polynomial.l1Norm_eq_zero_iff {A : Type u_2} [NormedRing A] (P : Polynomial A) : P.l1Norm = 0 ↔ P = 0

Over a normed ring, the coefficient l¹-norm vanishes exactly for the zero polynomial.

theorem Polynomial.l1Norm_add_le {R : Type u_1} [SeminormedRing R] (P Q : Polynomial R) : (P + Q).l1Norm ≤ P.l1Norm + Q.l1Norm

The coefficient l¹-norm satisfies the triangle inequality.

theorem Polynomial.l1Norm_sub_le {R : Type u_1} [SeminormedRing R] (P Q : Polynomial R) : (P - Q).l1Norm ≤ P.l1Norm + Q.l1Norm

The coefficient l¹-norm of a difference is at most the sum of the coefficient l¹-norms.

theorem Polynomial.l1Norm_sum_le {R : Type u_1} [SeminormedRing R] {S : Type u_2} (s : Finset S) (P : S → Polynomial R) : (∑ i ∈ s, P i).l1Norm ≤ ∑ i ∈ s, (P i).l1Norm

The coefficient l¹-norm of a finite sum is at most the sum of the coefficient l¹-norms.

theorem Polynomial.l1Norm_mul_le {R : Type u_1} [SeminormedRing R] (P Q : Polynomial R) : (P * Q).l1Norm ≤ P.l1Norm * Q.l1Norm

The coefficient l¹-norm is submultiplicative.

theorem Polynomial.norm_eval_le_l1Norm_mul {R : Type u_1} [SeminormedRing R] (P : Polynomial R) (z : R) : ‖eval z P‖ ≤ P.l1Norm * max 1 ‖z‖ ^ P.natDegree

Evaluation is controlled by coefficient length and the largest power of the evaluation point permitted by the degree.

theorem Polynomial.norm_eval_le_add_one_mul_supNorm_mul {R : Type u_1} [SeminormedRing R] {P : Polynomial R} {n : ℕ} (hP : P.natDegree ≤ n) (z : R) : ‖eval z P‖ ≤ (↑n + 1) * P.supNorm * max 1 ‖z‖ ^ n

Evaluation is controlled by the coefficient sup norm: for P of degree at most n, ‖P(z)‖ ≤ (n + 1) ‖P‖_∞ max(1, ‖z‖) ^ n.

theorem Polynomial.l1Norm_pow_le_of_ne_zero {R : Type u_1} [SeminormedRing R] (P : Polynomial R) {n : ℕ} (hn : n ≠ 0) : (P ^ n).l1Norm ≤ P.l1Norm ^ n

Taking a positive power raises the coefficient l¹-norm by at most the same power.

theorem Polynomial.l1Norm_pow_le {R : Type u_1} [SeminormedRing R] [NormOneClass R] (P : Polynomial R) (n : ℕ) : (P ^ n).l1Norm ≤ P.l1Norm ^ n

Taking a power raises the coefficient l¹-norm by at most the same power.

theorem Polynomial.l1Norm_comp_le {R : Type u_1} [SeminormedRing R] (P Q : Polynomial R) : (P.comp Q).l1Norm ≤ P.l1Norm * max 1 Q.l1Norm ^ P.natDegree

The coefficient l¹-norm of a composition P.comp Q is at most that of P times max 1 Q.l1Norm ^ P.natDegree.

theorem Polynomial.l1Norm_C_mul_X_add_C_le {R : Type u_1} [SeminormedRing R] (c d : R) : (C c * X + C d).l1Norm ≤ ‖c‖ + ‖d‖

The coefficient l¹-norm of the linear polynomial C c * X + C d is at most ‖c‖ + ‖d‖.

theorem Polynomial.l1Norm_mul_X_add_C_le {R : Type u_1} [SeminormedRing R] (Q : Polynomial R) (a : R) : (Q * (X + C a)).l1Norm ≤ Q.l1Norm * (1 + ‖a‖)

Multiplying by X + C a multiplies the coefficient l¹-norm by at most 1 + ‖a‖.

theorem Polynomial.l1Norm_comp_X_add_C_le {R : Type u_1} [SeminormedRing R] (P : Polynomial R) (a : R) : (P.comp (X + C a)).l1Norm ≤ P.l1Norm * (1 + ‖a‖) ^ P.natDegree

The coefficient l¹-norm of the translate P.comp (X + C a) is at most (1 + ‖a‖) ^ natDegree times that of P.

theorem Polynomial.l1Norm_hasseDeriv_le {R : Type u_1} [SeminormedRing R] (P : Polynomial R) (k : ℕ) : ((hasseDeriv k) P).l1Norm ≤ 2 ^ P.natDegree * P.l1Norm

The coefficient l¹-norm of the k-th Hasse derivative is at most 2 ^ natDegree times that of P.

theorem Polynomial.l1Norm_hasseDeriv_le_pow {R : Type u_1} [SeminormedRing R] {P : Polynomial R} {k r : ℕ} {δ C₁ : ℝ} (hP : ↑P.natDegree ≤ δ * ↑r) (hPC : P.l1Norm ≤ C₁ ^ r) : ((hasseDeriv k) P).l1Norm ≤ (2 ^ δ) ^ r * C₁ ^ r

The coefficient length of a Hasse derivative of P is at most (2 ^ δ) ^ r C₁ ^ r when P has degree at most δ r and coefficient length at most C₁ ^ r.

theorem Polynomial.norm_eval_le_l1Norm_mul_of_mul_X_sub_C_pow_eq {A : Type u_2} [SeminormedCommRing A] {V W : Polynomial A} {a z : A} {m : ℕ} (h : V * (X - C a) ^ m = W) (hz : ‖z - a‖ ≤ 1) : ‖eval z V‖ ≤ W.l1Norm * (1 + ‖a‖) ^ W.natDegree

If V * (X - a) ^ m = W, then V is bounded on the closed unit ball around a by the coefficient l¹-norm of W times (1 + ‖a‖) ^ natDegree W.

theorem Polynomial.l1Norm_aeval_homogenize_le {A : Type u_2} [SeminormedCommRing A] (p : Polynomial A) (n : ℕ) (g h : Polynomial A) : ((MvPolynomial.aeval ![g, h]) (p.homogenize n)).l1Norm ≤ p.supNorm * (g.l1Norm + h.l1Norm) ^ n

Substituting g and h for the two variables of the homogenization of degree n of p gives a polynomial of coefficient l¹-norm at most ‖p‖∞ (‖g‖₁ + ‖h‖₁) ^ n, where ‖p‖∞ is the coefficient sup norm of p.