Total ℓ₁ Coefficient Norm of Bivariate Integer Polynomials

This module defines the total bivariate ℓ₁ coefficient norm Polynomial.bivariateCoeffNorm1 of a polynomial P : Polynomial (Polynomial ℤ) (representing P(T, V) ∈ ℤ[T][V]), defined as the sum over s ∈ P.support of (P.coeff s).coeffNorm1, and proves its basic triangle and submultiplicativity inequalities. These bounds are used in Appendix B.2 of OpenAI, The Exponential Time Hypothesis is False to bound the coefficient size of cleared-denominator parity-amplifier products.

Main definitions

• Polynomial.bivariateCoeffNorm1: the total ℓ₁ norm ∑ s ∈ P.support, (P.coeff s).coeffNorm1 of P : Polynomial (Polynomial ℤ).

Main results

• Polynomial.coeffNorm1_coeff_le_bivariateCoeffNorm1: every V^s-coefficient has coeffNorm1 at most P.bivariateCoeffNorm1.
• Polynomial.bivariateCoeffNorm1_add_le, Polynomial.bivariateCoeffNorm1_sum_le: triangle inequalities for bivariateCoeffNorm1.
• Polynomial.bivariateCoeffNorm1_mul_le, Polynomial.bivariateCoeffNorm1_prod_le: submultiplicativity of bivariateCoeffNorm1 on Polynomial (Polynomial ℤ).

noncomputable def Polynomial.bivariateCoeffNorm1 (P : Polynomial (Polynomial ℤ)) : ℕ

The total bivariate ℓ₁ coefficient norm ∑ s ∈ P.support, (P.coeff s).coeffNorm1 of a polynomial P : Polynomial (Polynomial ℤ).

@[simp]

theorem Polynomial.bivariateCoeffNorm1_zero : bivariateCoeffNorm1 0 = 0

bivariateCoeffNorm1 0 = 0.

@[simp]

theorem Polynomial.bivariateCoeffNorm1_C (c : Polynomial ℤ) : (C c).bivariateCoeffNorm1 = c.coeffNorm1

bivariateCoeffNorm1 (C c) = c.coeffNorm1.

@[simp]

theorem Polynomial.bivariateCoeffNorm1_one : bivariateCoeffNorm1 1 = 1

bivariateCoeffNorm1 1 = 1.

theorem Polynomial.coeffNorm1_coeff_le_bivariateCoeffNorm1 (P : Polynomial (Polynomial ℤ)) (s : ℕ) : (P.coeff s).coeffNorm1 ≤ P.bivariateCoeffNorm1

Every V^s-coefficient of P has coeffNorm1 at most P.bivariateCoeffNorm1.

theorem Polynomial.bivariateCoeffNorm1_eq_sum_of_support_subset {P : Polynomial (Polynomial ℤ)} {S : Finset ℕ} (hS : P.support ⊆ S) : P.bivariateCoeffNorm1 = ∑ s ∈ S, (P.coeff s).coeffNorm1

If P.support ⊆ S, then P.bivariateCoeffNorm1 = ∑ s ∈ S, (P.coeff s).coeffNorm1.

theorem Polynomial.bivariateCoeffNorm1_add_le (P Q : Polynomial (Polynomial ℤ)) : (P + Q).bivariateCoeffNorm1 ≤ P.bivariateCoeffNorm1 + Q.bivariateCoeffNorm1

Triangle inequality for bivariateCoeffNorm1.

theorem Polynomial.bivariateCoeffNorm1_sum_le {α : Type u_1} (s : Finset α) (f : α → Polynomial (Polynomial ℤ)) : (∑ a ∈ s, f a).bivariateCoeffNorm1 ≤ ∑ a ∈ s, (f a).bivariateCoeffNorm1

Finite-sum triangle inequality for bivariateCoeffNorm1.

theorem Polynomial.bivariateCoeffNorm1_C_mul_le (c : Polynomial ℤ) (P : Polynomial (Polynomial ℤ)) : (C c * P).bivariateCoeffNorm1 ≤ c.coeffNorm1 * P.bivariateCoeffNorm1

Multiplying by C c (c : Polynomial ℤ) scales bivariateCoeffNorm1 by at most c.coeffNorm1.

theorem Polynomial.bivariateCoeffNorm1_mul_X_pow_le (P : Polynomial (Polynomial ℤ)) (k : ℕ) : (P * X ^ k).bivariateCoeffNorm1 ≤ P.bivariateCoeffNorm1

Multiplying by X ^ k does not increase bivariateCoeffNorm1.

theorem Polynomial.bivariateCoeffNorm1_mul_le (P Q : Polynomial (Polynomial ℤ)) : (P * Q).bivariateCoeffNorm1 ≤ P.bivariateCoeffNorm1 * Q.bivariateCoeffNorm1

bivariateCoeffNorm1 is submultiplicative on Polynomial (Polynomial ℤ).

theorem Polynomial.bivariateCoeffNorm1_pow_le (P : Polynomial (Polynomial ℤ)) (n : ℕ) : (P ^ n).bivariateCoeffNorm1 ≤ P.bivariateCoeffNorm1 ^ n

bivariateCoeffNorm1 of a power is at most the power of bivariateCoeffNorm1.

theorem Polynomial.bivariateCoeffNorm1_prod_le {κ : Type u_1} (I : Finset κ) (F : κ → Polynomial (Polynomial ℤ)) : (∏ i ∈ I, F i).bivariateCoeffNorm1 ≤ ∏ i ∈ I, (F i).bivariateCoeffNorm1

bivariateCoeffNorm1 of a finite product is at most the product of the bivariateCoeffNorm1s.