Coefficient L1 norm of multivariate polynomials

DefinitionCoefficient L1 norm of a multivariate polynomial#✓fully proved

The rational sum of the absolute values of a polynomial's coefficients.

noncomputable def coeffL1Norm (p : MvPolynomial σ ℚ) : ℚ :=
  ∑ m ∈ p.support, |p.coeff m|

Used by 10

Used byTriangle inequality for the coefficient L1 norm · Coefficient L1 norm as a sum over a larger index set · Coefficient L1 norm of a monomial · Upper bound on the coefficient L1 norm of a monomial · Submultiplicativity of the coefficient L1 norm · Nonnegativity of the coefficient L1 norm · Coefficient L1 norm of a scalar multiple · Coefficient L1 norm of a finite sum · Coefficient L1 norm of the zero polynomial · Coefficient L1 norm as an \(\ell^1\) distance

TheoremCoefficient L1 norm as a sum over a larger index set#✓fully proved

Enlarging the summation set beyond the support does not change the sum.

theorem coeffL1Norm_eq_sum {p : MvPolynomial σ ℚ} {S : Finset (σ →₀ ℕ)}
    (hS : p.support ⊆ S) : coeffL1Norm p = ∑ m ∈ S, |p.coeff m|

Uses 1 · Used by 3

Statement usesCoefficient L1 norm of a multivariate polynomial

Used byTriangle inequality for the coefficient L1 norm · Coefficient L1 norm of a monomial · Coefficient L1 norm of a scalar multiple

TheoremNonnegativity of the coefficient L1 norm#✓fully proved

The coefficient L1 norm is nonnegative.

theorem coeffL1Norm_nonneg (p : MvPolynomial σ ℚ) : 0 ≤ coeffL1Norm p

Uses 1

Statement usesCoefficient L1 norm of a multivariate polynomial

TheoremCoefficient L1 norm of the zero polynomial#✓fully proved

The zero polynomial has coefficient L1 norm zero.

@[simp]
theorem coeffL1Norm_zero : coeffL1Norm (0 : MvPolynomial σ ℚ) = 0

Uses 1 · Used by 1

Statement usesCoefficient L1 norm of a multivariate polynomial

Used byCoefficient L1 norm of a finite sum

TheoremTriangle inequality for the coefficient L1 norm#✓fully proved

Adding polynomials increases the coefficient L1 norm by at most the sum.

theorem coeffL1Norm_add_le (p q : MvPolynomial σ ℚ) :
    coeffL1Norm (p + q) ≤ coeffL1Norm p + coeffL1Norm q

Uses 2 · Used by 1

Statement usesCoefficient L1 norm of a multivariate polynomial

Proof usesCoefficient L1 norm as a sum over a larger index set

Used byCoefficient L1 norm of a finite sum

TheoremCoefficient L1 norm of a finite sum#✓fully proved

The norm of a finite sum is bounded by the sum of the coefficient norms.

theorem coeffL1Norm_sum_le {ι : Type*} (s : Finset ι) (f : ι → MvPolynomial σ ℚ) :
    coeffL1Norm (∑ i ∈ s, f i) ≤ ∑ i ∈ s, coeffL1Norm (f i)

Uses 3 · Used by 1

Statement usesCoefficient L1 norm of a multivariate polynomial

Proof usesTriangle inequality for the coefficient L1 norm · Coefficient L1 norm of the zero polynomial

Used bySubmultiplicativity of the coefficient L1 norm

TheoremCoefficient L1 norm of a scalar multiple#✓fully proved

Rational scalar multiplication scales the norm by the scalar's absolute value.

@[simp]
theorem coeffL1Norm_smul (a : ℚ) (p : MvPolynomial σ ℚ) :
    coeffL1Norm (a • p) = |a| * coeffL1Norm p

Uses 2

Statement usesCoefficient L1 norm of a multivariate polynomial

Proof usesCoefficient L1 norm as a sum over a larger index set

TheoremCoefficient L1 norm of a monomial#✓fully proved

A monomial's coefficient L1 norm is the absolute value of its coefficient, including when the coefficient is zero.

@[simp]
theorem coeffL1Norm_monomial (m : σ →₀ ℕ) (a : ℚ) :
    coeffL1Norm (monomial m a) = |a|

Uses 2 · Used by 1

Statement usesCoefficient L1 norm of a multivariate polynomial

Proof usesCoefficient L1 norm as a sum over a larger index set

Used byUpper bound on the coefficient L1 norm of a monomial

TheoremUpper bound on the coefficient L1 norm of a monomial#✓fully proved

The coefficient L1 norm of a monomial is at most its absolute coefficient.

theorem coeffL1Norm_monomial_le (m : σ →₀ ℕ) (a : ℚ) :
    coeffL1Norm (monomial m a) ≤ |a|

Uses 2 · Used by 1

Statement usesCoefficient L1 norm of a multivariate polynomial

Proof usesCoefficient L1 norm of a monomial

Used bySubmultiplicativity of the coefficient L1 norm

TheoremSubmultiplicativity of the coefficient L1 norm#✓fully proved

The coefficient convolution in a product is bounded by the product of the coefficient L1 norms; cancellation can make this inequality strict.

theorem coeffL1Norm_mul_le (p q : MvPolynomial σ ℚ) :
    coeffL1Norm (p * q) ≤ coeffL1Norm p * coeffL1Norm q

Uses 3

Statement usesCoefficient L1 norm of a multivariate polynomial

Proof usesUpper bound on the coefficient L1 norm of a monomial · Coefficient L1 norm of a finite sum

TheoremCoefficient L1 norm as an \(\ell^1\) distance#✓fully proved

The real cast of the coefficient L1 norm agrees with the explicit exponent-one metric on the exact rational coefficient Finsupp carrier.

theorem dist_coeff_zero_eq_coeffL1Norm (p : MvPolynomial σ ℚ) :
    dist (WithLp.toLp ((1 : NNReal) : ENNReal) p.coeff)
      (WithLp.toLp ((1 : NNReal) : ENNReal) (0 : (σ →₀ ℕ) →₀ ℚ)) =
        (coeffL1Norm p : ℝ)

Uses 1

Statement usesCoefficient L1 norm of a multivariate polynomial

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.