The ℓ₁ coefficient norm of an integer polynomial

This module defines the ℓ₁ coefficient norm Polynomial.coeffNorm1 of a univariate integer polynomial p : ℤ[X]: $$\|p\|_1 = \sum_{i \in \mathrm{supp}(p)} |p_i|,$$ together with its basic triangle, scaling, shift, linear-factor, submultiplicative, and integer-cast inequalities used in Lemma 4.6, Lemma 5.1, and Appendix B of [OpenAI2026ETH].

Main definitions

• Polynomial.coeffNorm1: the ℓ₁ coefficient norm ∑ i ∈ p.support, (p.coeff i).natAbs.

Main results

• Polynomial.natAbs_coeff_le_coeffNorm1, Polynomial.sum_natAbs_coeff_le_coeffNorm1: individual and finite-subset coefficient bounds by coeffNorm1.
• Polynomial.coeffNorm1_add_le, Polynomial.coeffNorm1_sub_le, Polynomial.coeffNorm1_sum_le: triangle inequalities for binary sums, differences, and finite sums.
• Polynomial.coeffNorm1_C_mul_le, Polynomial.coeffNorm1_X_mul, Polynomial.coeffNorm1_mul_X_pow_le, Polynomial.coeffNorm1_C_sub_X_mul_le, Polynomial.coeffNorm1_one_sub_X_mul_le, Polynomial.coeffNorm1_one_sub_X_pow_mul_le: norm bounds under scalar multiplication, monomial shifts, and linear factors.
• Polynomial.coeffNorm1_mul_le, Polynomial.coeffNorm1_pow_le, Polynomial.coeffNorm1_prod_le: submultiplicativity for binary products, powers, and finite products.
• Polynomial.natCast_coeffNorm1: integer cast identity (p.coeffNorm1 : ℤ) = ∑ i ∈ p.support, |p.coeff i|.
• Polynomial.coeffNorm1_ofCoeffList: coeffNorm1 (ofCoeffList l) = (l.map Int.natAbs).sum.

References

• OpenAI, The Exponential Time Hypothesis is False (Lemma 4.6, Appendix B.1, and Appendix B.2)

def Polynomial.coeffNorm1 (p : Polynomial ℤ) : ℕ

The ℓ₁ coefficient norm ∑ i ∈ p.support, (p.coeff i).natAbs of an integer polynomial.

@[simp]

theorem Polynomial.coeffNorm1_zero : coeffNorm1 0 = 0

The ℓ₁ norm of 0 is 0.

theorem Polynomial.coeffNorm1_eq_sum_of_support_subset {p : Polynomial ℤ} {S : Finset ℕ} (hS : p.support ⊆ S) : p.coeffNorm1 = ∑ i ∈ S, (p.coeff i).natAbs

Sum expression for coeffNorm1 over any superset S ⊇ p.support.

theorem Polynomial.natAbs_coeff_le_coeffNorm1 (p : Polynomial ℤ) (k : ℕ) : (p.coeff k).natAbs ≤ p.coeffNorm1

Every individual coefficient of p has absolute value at most coeffNorm1 p.

theorem Polynomial.sum_natAbs_coeff_le_coeffNorm1 (p : Polynomial ℤ) (s : Finset ℕ) : ∑ i ∈ s, (p.coeff i).natAbs ≤ p.coeffNorm1

The sum of (p.coeff i).natAbs over any finite set of indices is at most coeffNorm1 p.

theorem Polynomial.coeffNorm1_C (a : ℤ) : (C a).coeffNorm1 = a.natAbs

The ℓ₁ norm of a constant polynomial C a is a.natAbs.

@[simp]

theorem Polynomial.coeffNorm1_one : coeffNorm1 1 = 1

The ℓ₁ norm of 1 is 1.

@[simp]

theorem Polynomial.coeffNorm1_neg (p : Polynomial ℤ) : (-p).coeffNorm1 = p.coeffNorm1

Negating a polynomial preserves coeffNorm1.

theorem Polynomial.coeffNorm1_add_le (p q : Polynomial ℤ) : (p + q).coeffNorm1 ≤ p.coeffNorm1 + q.coeffNorm1

Triangle inequality for coeffNorm1.

theorem Polynomial.coeffNorm1_sub_le (p q : Polynomial ℤ) : (p - q).coeffNorm1 ≤ p.coeffNorm1 + q.coeffNorm1

Difference triangle inequality for coeffNorm1.

theorem Polynomial.coeffNorm1_sum_le {ι : Type u_1} (s : Finset ι) (f : ι → Polynomial ℤ) : (∑ i ∈ s, f i).coeffNorm1 ≤ ∑ i ∈ s, (f i).coeffNorm1

Finite-sum triangle inequality for coeffNorm1.

theorem Polynomial.coeffNorm1_C_mul_le (a : ℤ) (p : Polynomial ℤ) : (C a * p).coeffNorm1 ≤ a.natAbs * p.coeffNorm1

Scaling by C a scales coeffNorm1 by at most a.natAbs.

theorem Polynomial.coeffNorm1_X_mul (p : Polynomial ℤ) : (X * p).coeffNorm1 = p.coeffNorm1

Multiplying by X preserves coeffNorm1.

theorem Polynomial.coeffNorm1_mul_X_pow_le (p : Polynomial ℤ) (k : ℕ) : (p * X ^ k).coeffNorm1 ≤ p.coeffNorm1

Multiplying by X ^ k does not increase coeffNorm1.

theorem Polynomial.coeffNorm1_C_sub_X_mul_le (a : ℤ) (p : Polynomial ℤ) : ((C a - X) * p).coeffNorm1 ≤ (a.natAbs + 1) * p.coeffNorm1

Multiplying by C a - X scales coeffNorm1 by at most a.natAbs + 1.

theorem Polynomial.coeffNorm1_one_sub_X_mul_le (p : Polynomial ℤ) : ((1 - X) * p).coeffNorm1 ≤ 2 * p.coeffNorm1

Multiplying by 1 - X increases coeffNorm1 by at most a factor of 2.

theorem Polynomial.coeffNorm1_one_sub_X_pow_mul_le (ℓ : ℕ) (p : Polynomial ℤ) : ((1 - X) ^ ℓ * p).coeffNorm1 ≤ 2 ^ ℓ * p.coeffNorm1

Multiplying by (1 - X) ^ ℓ increases coeffNorm1 by at most a factor of 2 ^ ℓ.

theorem Polynomial.coeffNorm1_mul_le (p q : Polynomial ℤ) : (p * q).coeffNorm1 ≤ p.coeffNorm1 * q.coeffNorm1

coeffNorm1 is submultiplicative on ℤ[X].

theorem Polynomial.coeffNorm1_pow_le (p : Polynomial ℤ) (k : ℕ) : (p ^ k).coeffNorm1 ≤ p.coeffNorm1 ^ k

coeffNorm1 (p ^ k) ≤ coeffNorm1 p ^ k.

theorem Polynomial.coeffNorm1_prod_le {ι : Type u_1} (s : Finset ι) (f : ι → Polynomial ℤ) : (∏ a ∈ s, f a).coeffNorm1 ≤ ∏ a ∈ s, (f a).coeffNorm1

coeffNorm1 of a finite product is at most the product of the coeffNorm1s.

theorem Polynomial.natCast_coeffNorm1 (p : Polynomial ℤ) : ↑p.coeffNorm1 = ∑ i ∈ p.support, |p.coeff i|

Casting coeffNorm1 p to ℤ gives the sum of integer absolute values |p.coeff i|.

theorem Polynomial.natCast_coeffNorm1_C (a : ℤ) : ↑(C a).coeffNorm1 = |a|

Integer-cast constant norm (coeffNorm1 (C a) : ℤ) = |a|.

theorem Polynomial.natCast_coeffNorm1_add_le (p q : Polynomial ℤ) : ↑(p + q).coeffNorm1 ≤ ↑p.coeffNorm1 + ↑q.coeffNorm1

Integer-cast triangle inequality for coeffNorm1.

theorem Polynomial.natCast_coeffNorm1_sum_le {ι : Type u_1} (s : Finset ι) (f : ι → Polynomial ℤ) : ↑(∑ i ∈ s, f i).coeffNorm1 ≤ ∑ i ∈ s, ↑(f i).coeffNorm1

Integer-cast finite-sum triangle inequality for coeffNorm1.

theorem Polynomial.natCast_coeffNorm1_C_mul_le (a : ℤ) (p : Polynomial ℤ) : ↑(C a * p).coeffNorm1 ≤ |a| * ↑p.coeffNorm1

Integer-cast scalar multiplication bound for coeffNorm1.

@[simp]

theorem Polynomial.coeffNorm1_ofCoeffList (l : List ℤ) : (ofCoeffList l).coeffNorm1 = (List.map Int.natAbs l).sum

The ℓ₁ coefficient norm of ofCoeffList l equals the sum of Int.natAbs of l.