The coefficient ℓ¹-norm of integer multivariate polynomials

MvPolynomial.l1Norm f is the sum of the absolute values of the coefficients of an integer polynomial f, as a natural number.

Main results

• MvPolynomial.l1Norm_add_le, MvPolynomial.l1Norm_mul_le, MvPolynomial.l1Norm_sum_le, MvPolynomial.l1Norm_prod_le, MvPolynomial.l1Norm_pow_le: the norm is subadditive and submultiplicative.
• MvPolynomial.l1Norm_det_le: the norm of a determinant is at most n! * L ^ n when every entry has norm at most L.
• MvPolynomial.l1Norm_rename_le: renaming variables does not increase the norm.
• MvPolynomial.l1Norm_coeff_le_l1Norm_sumAlgEquiv_symm: a coefficient of a polynomial with polynomial coefficients has norm at most that of the flattened polynomial.

def MvPolynomial.l1Norm {σ : Type u_1} (f : MvPolynomial σ ℤ) : ℕ

The sum of the absolute values of all coefficients of an integer polynomial.

Equations

• f.l1Norm = ∑ m ∈ f.support, (f.coeff m).natAbs

@[simp]

theorem MvPolynomial.l1Norm_zero {σ : Type u_1} : l1Norm 0 = 0

The zero polynomial has ℓ¹-norm zero.

theorem MvPolynomial.l1Norm_eq_sum_of_support_subset {σ : Type u_1} (f : MvPolynomial σ ℤ) (s : Finset (σ →₀ ℕ)) (hs : f.support ⊆ s) : f.l1Norm = ∑ m ∈ s, (f.coeff m).natAbs

The ℓ¹-norm of f is the sum of the absolute values of its coefficients over any finite set s of exponents containing the support of f.

theorem MvPolynomial.natAbs_coeff_le_l1Norm {σ : Type u_1} (f : MvPolynomial σ ℤ) (m : σ →₀ ℕ) : (f.coeff m).natAbs ≤ f.l1Norm

Each coefficient of f has absolute value at most the ℓ¹-norm of f.

@[simp]

theorem MvPolynomial.l1Norm_monomial {σ : Type u_1} (m : σ →₀ ℕ) (c : ℤ) : ((monomial m) c).l1Norm = c.natAbs

The ℓ¹-norm of the monomial monomial m c is the absolute value of c.

theorem MvPolynomial.l1Norm_C {σ : Type u_1} (c : ℤ) : (C c).l1Norm = c.natAbs

The ℓ¹-norm of the constant polynomial C c is the absolute value of c.

@[simp]

theorem MvPolynomial.l1Norm_intCast {σ : Type u_1} (c : ℤ) : (↑c).l1Norm = c.natAbs

An integer cast has ℓ¹-norm equal to its absolute value.

@[simp]

theorem MvPolynomial.l1Norm_one {σ : Type u_1} : l1Norm 1 = 1

The constant polynomial 1 has ℓ¹-norm one.

theorem MvPolynomial.l1Norm_add_le {σ : Type u_1} (f g : MvPolynomial σ ℤ) : (f + g).l1Norm ≤ f.l1Norm + g.l1Norm

The ℓ¹-norm is subadditive.

theorem MvPolynomial.l1Norm_sum_le {σ : Type u_1} {ι : Type u_2} (s : Finset ι) (f : ι → MvPolynomial σ ℤ) : (∑ i ∈ s, f i).l1Norm ≤ ∑ i ∈ s, (f i).l1Norm

The ℓ¹-norm of a finite sum is at most the sum of the ℓ¹-norms of the summands.

theorem MvPolynomial.l1Norm_mul_le {σ : Type u_1} (f g : MvPolynomial σ ℤ) : (f * g).l1Norm ≤ f.l1Norm * g.l1Norm

The ℓ¹-norm is submultiplicative.

theorem MvPolynomial.l1Norm_prod_le {σ : Type u_1} {ι : Type u_2} (s : Finset ι) (f : ι → MvPolynomial σ ℤ) : (∏ i ∈ s, f i).l1Norm ≤ ∏ i ∈ s, (f i).l1Norm

The ℓ¹-norm of a finite product is at most the product of the ℓ¹-norms of the factors.

theorem MvPolynomial.l1Norm_pow_le {σ : Type u_2} (f : MvPolynomial σ ℤ) (n : ℕ) : (f ^ n).l1Norm ≤ f.l1Norm ^ n

The ℓ¹-norm of f ^ n is at most the n-th power of the ℓ¹-norm of f.

@[simp]

theorem MvPolynomial.l1Norm_neg {σ : Type u_1} (f : MvPolynomial σ ℤ) : (-f).l1Norm = f.l1Norm

Negation preserves the ℓ¹-norm.

@[simp]

theorem MvPolynomial.l1Norm_units_smul {σ : Type u_1} (u : ℤˣ) (f : MvPolynomial σ ℤ) : (u • f).l1Norm = f.l1Norm

Multiplication by an integer unit, that is by ±1, preserves the ℓ¹-norm.

theorem MvPolynomial.l1Norm_det_le {σ : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (M : Matrix ι ι (MvPolynomial σ ℤ)) (L : ℕ) (hM : ∀ (i j : ι), (M i j).l1Norm ≤ L) : M.det.l1Norm ≤ (Fintype.card ι).factorial * L ^ Fintype.card ι

If every entry of a square matrix M of integer polynomials has ℓ¹-norm at most L, then the determinant of M has ℓ¹-norm at most n! * L ^ n, where n is the size of M.

theorem MvPolynomial.l1Norm_rename_le {σ : Type u_2} {τ : Type u_3} (v : σ → τ) (f : MvPolynomial σ ℤ) : ((rename v) f).l1Norm ≤ f.l1Norm

Renaming the variables along any map v does not increase the ℓ¹-norm.

theorem MvPolynomial.coeff_sumAlgEquiv_symm {σ : Type u_2} {τ : Type u_3} (f : MvPolynomial σ (MvPolynomial τ ℤ)) (m : σ →₀ ℕ) (n : τ →₀ ℕ) : ((sumAlgEquiv ℤ σ τ).symm f).coeff (Finsupp.sumFinsuppAddEquivProdFinsupp.symm (m, n)) = (f.coeff m).coeff n

The coefficient of the flattened polynomial (sumAlgEquiv ℤ σ τ).symm f at the exponent on σ ⊕ τ assembled from m and n is the coefficient at n of the coefficient of f at m.

theorem MvPolynomial.l1Norm_coeff_le_l1Norm_sumAlgEquiv_symm {σ : Type u_2} {τ : Type u_3} (f : MvPolynomial σ (MvPolynomial τ ℤ)) (m : σ →₀ ℕ) : (f.coeff m).l1Norm ≤ ((sumAlgEquiv ℤ σ τ).symm f).l1Norm

Extracting one outer coefficient never increases the total coefficient sum after flattening the two variable families.

theorem MvPolynomial.sumAlgEquiv_symm_map_C {σ : Type u_2} {τ : Type u_3} (p : MvPolynomial σ ℤ) : (sumAlgEquiv ℤ σ τ).symm ((map C) p) = (rename Sum.inl) p

Flattening a polynomial whose coefficients are constants of MvPolynomial τ ℤ renames its variables into the left summand of σ ⊕ τ.

theorem MvPolynomial.l1Norm_sumAlgEquiv_symm_C_X_mul_map_C_le {σ : Type u_2} {τ : Type u_3} (p : MvPolynomial σ ℤ) (i : τ) : ((sumAlgEquiv ℤ σ τ).symm (C (X i) * (map C) p)).l1Norm ≤ p.l1Norm

One original coefficient variable multiplying an integer parameter polynomial has no coefficient-norm cost beyond that parameter polynomial.