Polynomials as lists of their low coefficients

Mathlib's Polynomial.ofCoeffList builds a polynomial from its coefficients, the constant coefficient first. This file evaluates such a polynomial by Horner's rule on the list (Polynomial.evalCoeffList), bounds its degree by the length of the list less one, lists the first n coefficients of a polynomial (Polynomial.coeffsBelow), which give the polynomial back when its degree is less than n. An interactive verifier receives polynomials in this form.

Main definitions

• Polynomial.evalCoeffList: Horner evaluation of a coefficient list.
• Polynomial.coeffsBelow: the coefficients of X ^ 0, …, X ^ (n - 1).

Main results

• Polynomial.eval_ofCoeffList: evaluation is Horner's rule.
• Polynomial.natDegree_ofCoeffList_le: the degree is at most the length of the list less one.
• Polynomial.ofCoeffList_coeffsBelow: low coefficients determine a polynomial of small degree.

def Polynomial.evalCoeffList {R : Type u_1} [Semiring R] (z : R) (l : List R) : R

The value at z of the polynomial with coefficient list l, the constant coefficient first, by Horner's rule.

@[simp]

theorem Polynomial.evalCoeffList_nil {R : Type u_1} [Semiring R] (z : R) : evalCoeffList z [] = 0

The empty coefficient list evaluates to 0.

@[simp]

theorem Polynomial.evalCoeffList_cons {R : Type u_1} [Semiring R] (z a : R) (l : List R) : evalCoeffList z (a :: l) = a + z * evalCoeffList z l

Horner's step: a :: l evaluates to a + z * evalCoeffList z l.

theorem Polynomial.eval_ofCoeffList {R : Type u_2} [CommSemiring R] (z : R) (l : List R) : eval z (ofCoeffList l) = evalCoeffList z l

The value of the polynomial with coefficient list l is given by Horner's rule.

theorem Polynomial.natDegree_ofCoeffList_le {R : Type u_1} [Semiring R] (l : List R) : (ofCoeffList l).natDegree ≤ l.length - 1

The polynomial with coefficient list l has degree at most l.length - 1.

def Polynomial.coeffsBelow {R : Type u_1} [Semiring R] (P : Polynomial R) (n : ℕ) : List R

The coefficients of X ^ 0, …, X ^ (n - 1) of a polynomial, in this order.

@[simp]

theorem Polynomial.length_coeffsBelow {R : Type u_1} [Semiring R] (P : Polynomial R) (n : ℕ) : (P.coeffsBelow n).length = n

coeffsBelow P n has length n.

theorem Polynomial.ofCoeffList_coeffsBelow {R : Type u_1} [Semiring R] {P : Polynomial R} {n : ℕ} (hP : P.natDegree < n) : ofCoeffList (P.coeffsBelow n) = P

The first n coefficients of a polynomial of degree less than n give the polynomial back.