Coefficients of products with linear factors

TheoremCoefficients of a product with a homogeneous linear polynomial#✓fully proved

The coefficient of p * q, when p is homogeneous of degree one, is the sum obtained by removing one occurrence of each variable in the monomial.

public theorem IsHomogeneous.coeff_mul_eq_sum_support {σ R : Type*} [CommSemiring R]
    {p : MvPolynomial σ R} (hp : p.IsHomogeneous 1) (q : MvPolynomial σ R)
    (m : σ →₀ ℕ) :
    (p * q).coeff m =
      ∑ i ∈ m.support, p.coeff (Finsupp.single i 1) *
        q.coeff (m - Finsupp.single i 1)

DefinitionCoefficient list after multiplication by a linear polynomial#✓fully proved

The dense little-endian coefficients after left multiplication by C r + X * C c.

def mulLinearCoeffList (r c : R) (l : List R) : List R :=
  List.zipWithAll (fun a b => a.getD 0 + b.getD 0)
    (l.map (r * ·)) ((0 :: l).map (c * ·))

Used by 3

Used byCoefficient recurrence for multiplication by a linear polynomial · Length of the coefficient list after a linear multiplication · Coefficient-list multiplication agrees with polynomial multiplication

TheoremLength of the coefficient list after a linear multiplication#✓fully proved

A linear-coefficient update always adds one dense coefficient.

@[simp] theorem length_mulLinearCoeffList (r c : R) (l : List R) :
    (mulLinearCoeffList r c l).length = l.length + 1

Uses 1

Statement usesCoefficient list after multiplication by a linear polynomial

TheoremCoefficient recurrence for multiplication by a linear polynomial#✓fully proved

The coefficient at every index, including beyond the dense output, follows the source recurrence r * l[j] + c * l[j - 1].

@[simp] theorem getD_mulLinearCoeffList (r c : R) (l : List R) (j : ℕ) :
    (mulLinearCoeffList r c l).getD j 0 =
      r * l.getD j 0 + c * (0 :: l).getD j 0

Uses 1

Statement usesCoefficient list after multiplication by a linear polynomial

TheoremCoefficient-list multiplication agrees with polynomial multiplication#✓fully proved

Interpreting the dense output as a little-endian polynomial is left multiplication by the linear polynomial C r + X * C c.

@[simp] theorem ofCoeffList_mulLinearCoeffList (r c : R) (l : List R) :
    ofCoeffList (mulLinearCoeffList r c l) =
      (C r + X * C c) * ofCoeffList l

Uses 1

Statement usesCoefficient list after multiplication by a linear polynomial

TheoremExpansion of a product of affine linear polynomials#✓fully proved

Expand a product of affine linear polynomials by the subset of factors from which the linear term is selected.

theorem prod_C_add_X_mul_C_eq_sum {ι R : Type*} [DecidableEq ι]
    [CommSemiring R]
    (S : Finset ι) (r c : ι → R) :
    ∏ s ∈ S, (C (r s) + X * C (c s)) =
      ∑ Q ∈ S.powerset,
        C (∏ s ∈ S, if s ∈ Q then c s else r s) * X ^ #Q

Used by 1

Used byCoefficients of a product of affine linear polynomials

TheoremCoefficients of a product of affine linear polynomials#✓fully proved

The coefficient of degree i in a product of affine linear polynomials is the sum over the i factors from which the linear term is selected.

theorem prod_C_add_X_mul_C_coeff {ι R : Type*} [DecidableEq ι]
    [CommSemiring R] (S : Finset ι) (r c : ι → R) (i : ℕ) :
    (∏ s ∈ S, (C (r s) + X * C (c s))).coeff i =
      ∑ Q ∈ S.powersetCard i,
        ∏ s ∈ S, if s ∈ Q then c s else r s

Uses 1 · Used by 1

Proof usesExpansion of a product of affine linear polynomials

Used byBinomial bound on coefficients of a product of affine polynomials

TheoremDegree bound for a product of affine linear polynomials#✓fully proved

A product of affine linear polynomials has degree at most the number of factors.

theorem prod_C_add_X_mul_C_natDegree_le {ι R : Type*} [CommSemiring R]
    (S : Finset ι) (r c : ι → R) :
    (∏ s ∈ S, (C (r s) + X * C (c s))).natDegree ≤ #S

TheoremBinomial bound on coefficients of a product of affine polynomials#✓fully proved

If every constant and linear coefficient is at most one in absolute value, then the absolute value of coefficient i is at most S.card.choose i.

theorem abs_prod_C_add_X_mul_C_coeff_le_choose {ι : Type*} [DecidableEq ι]
    (S : Finset ι) (r c : ι → ℤ) (i : ℕ)
    (hr : ∀ s ∈ S, |r s| ≤ 1) (hc : ∀ s ∈ S, |c s| ≤ 1) :
    |(∏ s ∈ S, (C (r s) + X * C (c s))).coeff i| ≤
      ((#S).choose i : ℤ)

Uses 1

Proof usesCoefficients of a product of affine linear polynomials

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.