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.

Splitting a list splits the polynomial: l₁ ++ l₂ gives ofCoeffList l₁ + X ^ l₁.length * ofCoeffList l₂ (Polynomial.ofCoeffList_append). Padding with zeros does not change it (Polynomial.ofCoeffList_takeD_of_length_le), and the zero-padded first m + k coefficients split into the first m and the next k (Polynomial.ofCoeffList_takeD_add). Divide-and-conquer multiplication of coefficient lists uses these splits.

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.
• Polynomial.ofCoeffList_append: concatenation is a shifted sum.
• Polynomial.ofCoeffList_takeD_of_length_le, Polynomial.ofCoeffList_takeD_add: zero padding and splitting a padded prefix.

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.

theorem Polynomial.ofCoeffList_append {R : Type u_1} [Semiring R] (l₁ l₂ : List R) : ofCoeffList (l₁ ++ l₂) = ofCoeffList l₁ + X ^ l₁.length * ofCoeffList l₂

Concatenating coefficient lists shifts the second polynomial past the first.

theorem Polynomial.ofCoeffList_eq_C_headD_add_X_mul_tail {R : Type u_1} [Semiring R] (l : List R) : ofCoeffList l = C (l.headD 0) + X * ofCoeffList l.tail

Peeling the constant coefficient, with 0 for the empty list.

@[simp]

theorem Polynomial.ofCoeffList_replicate_zero {R : Type u_1} [Semiring R] (n : ℕ) : ofCoeffList (List.replicate n 0) = 0

A list of zeros is the zero polynomial.

theorem Polynomial.ofCoeffList_takeD_of_length_le {R : Type u_1} [Semiring R] {l : List R} {n : ℕ} (h : l.length ≤ n) : ofCoeffList (List.takeD n l 0) = ofCoeffList l

Padding a coefficient list with zeros does not change the polynomial.

theorem Polynomial.ofCoeffList_takeD_add {R : Type u_1} [Semiring R] (l : List R) (m k : ℕ) : ofCoeffList (List.takeD (m + k) l 0) = ofCoeffList (List.takeD m l 0) + X ^ m * ofCoeffList (List.takeD k (List.drop m l) 0)

The zero-padded first m + k coefficients split into the first m and the next k.