Evaluation matrices and auxiliary polynomials

A coefficient vector in the kernel of the monomial evaluation matrix produces a polynomial vanishing at every specified point. Injectivity of the list of monomials ensures that a nonzero vector produces a nonzero polynomial.

noncomputable def CCDN.polynomialOfCoefficients {n N : ℕ} (mon : Fin N → Fin n →₀ ℕ) (v : Fin N → ℤ) : MvPolynomial (Fin n) ℤ

The integer polynomial ∑ j, v j * X ^ mon j with coefficient vector v on the list of monomials mon.

Equations

• CCDN.polynomialOfCoefficients mon v = ∑ j : Fin N, (MvPolynomial.monomial (mon j)) (v j)

theorem CCDN.coefficient_polynomialOfCoefficients {n N : ℕ} (mon : Fin N → Fin n →₀ ℕ) (hmon : Function.Injective mon) (v : Fin N → ℤ) (j : Fin N) : (polynomialOfCoefficients mon v).coeff (mon j) = v j

For an injective list of monomials mon, the coefficient of mon j in polynomialOfCoefficients mon v is v j.

theorem CCDN.polynomialOfCoefficients_ne_zero {n N : ℕ} (mon : Fin N → Fin n →₀ ℕ) (hmon : Function.Injective mon) {v : Fin N → ℤ} (hv : v ≠ 0) : polynomialOfCoefficients mon v ≠ 0

For an injective list of monomials, a nonzero coefficient vector gives a nonzero polynomial.

theorem CCDN.totalDegree_polynomialOfCoefficients_le {n N M : ℕ} (mon : Fin N → Fin n →₀ ℕ) (v : Fin N → ℤ) (hdeg : ∀ (j : Fin N), Finsupp.degree (mon j) ≤ M) : (polynomialOfCoefficients mon v).totalDegree ≤ M

If every monomial in the list mon has degree at most M, then polynomialOfCoefficients mon v has total degree at most M.

noncomputable def CCDN.evaluationMatrix {n N s : ℕ} (mon : Fin N → Fin n →₀ ℕ) (points : Fin s → Fin n → ℤ) : Matrix (Fin s) (Fin N) ℤ

The monomial evaluation matrix, whose entry in row i and column j is the value of the monomial mon j at the integer point points i.

Equations

• CCDN.evaluationMatrix mon points i j = (mon j).prod fun (k : Fin n) (e : ℕ) => points i k ^ e

theorem CCDN.eval_polynomialOfCoefficients {n N s : ℕ} (mon : Fin N → Fin n →₀ ℕ) (points : Fin s → Fin n → ℤ) (v : Fin N → ℤ) (i : Fin s) : (MvPolynomial.eval (points i)) (polynomialOfCoefficients mon v) = (evaluationMatrix mon points).mulVec v i

The value of polynomialOfCoefficients mon v at points i is the i-th entry of the product of the monomial evaluation matrix with v.

theorem CCDN.abs_monomial_value_le {n M : ℕ} (e : Fin n →₀ ℕ) (x : Fin n → ℤ) {B : ℝ} (hB : 1 ≤ B) (hx : InBox x B) (he : Finsupp.degree e ≤ M) : |↑(e.prod fun (i : Fin n) (k : ℕ) => x i ^ k)| ≤ B ^ M

If the integer point x lies in the box of radius B ≥ 1 and the exponent e has degree at most M, then the monomial x ^ e has absolute value at most B ^ M.