Polynomials from a list of coefficients, and division by a monic polynomial

Polynomial is a Finsupp, so none of its arithmetic reduces in the kernel. A polynomial presented instead by the list of its coefficients does compute, and this file sets up the translation, together with the one algorithm a computation on such lists needs: division by a monic polynomial.

TauCeti.Polynomial.ofCoeffList l is the polynomial whose coefficients are the entries of l, read from the highest degree down, so that it inverts Mathlib's Polynomial.coeffList (TauCeti.Polynomial.coeffList_ofCoeffList and TauCeti.Polynomial.ofCoeffList_coeffList). Its defining recursion is Horner's, ofCoeffList (l ++ [a]) = ofCoeffList l * X + C a, and every proof below runs along it. It is a noncomputable specification map: the lists are what compute.

TauCeti.Polynomial.mulCoeffList multiplies two such lists by convolving their coefficients, and TauCeti.Polynomial.ofCoeffList_mulCoeffList identifies the result with the product polynomial.

TauCeti.Polynomial.divModByMonicList t l is long division of ofCoeffList l by the monic polynomial X ^ t.length + ofCoeffList t, carried out as the usual synthetic division: a window of t.length remainder coefficients is carried along the dividend, and at each step the coefficient shifted out of the window is the next quotient coefficient and is used to clear the window against the divisor. Presenting the divisor by the list t of the coefficients below its leading one makes it monic by construction, so TauCeti.Polynomial.ofCoeffList_divByMonicList and TauCeti.Polynomial.ofCoeffList_modByMonicList, which identify the two outputs with Mathlib's /ₘ and %ₘ, need no hypotheses at all. Like Mathlib's /ₘ and %ₘ, the division needs no commutativity: the window is cleared by x - y * c, with the quotient coefficient c on the right, which is what matches Mathlib's convention f = g * q + r with the divisor on the left.

The division definitions are @[expose]d, since a consumer computing with them in another module reduces them in the kernel.

noncomputable def TauCeti.Polynomial.ofCoeffList {R : Type u_1} [Semiring R] (l : List R) : Polynomial R

The polynomial whose coefficients are the entries of l, highest degree first: ofCoeffList [a, b, c] = C a * X ^ 2 + C b * X + C c. This is Horner's rule, and it inverts Mathlib's Polynomial.coeffList (TauCeti.Polynomial.coeffList_ofCoeffList).

Equations

• TauCeti.Polynomial.ofCoeffList l = List.foldl (fun (p : Polynomial R) (a : R) => p * Polynomial.X + Polynomial.C a) 0 l

@[simp]

theorem TauCeti.Polynomial.ofCoeffList_nil {R : Type u_1} [Semiring R] : ofCoeffList [] = 0

The empty list of coefficients defines the zero polynomial.

@[simp]

theorem TauCeti.Polynomial.ofCoeffList_concat {R : Type u_1} [Semiring R] (l : List R) (a : R) : ofCoeffList (l ++ [a]) = ofCoeffList l * Polynomial.X + Polynomial.C a

The Horner recursion defining TauCeti.Polynomial.ofCoeffList: appending the coefficient a at the bottom multiplies the polynomial so far by X and adds the constant C a.

@[simp]

theorem TauCeti.Polynomial.coeff_ofCoeffList {R : Type u_1} [Semiring R] (l : List R) (i : ℕ) : (ofCoeffList l).coeff i = l.reverse.getD i 0

The coefficients of TauCeti.Polynomial.ofCoeffList l are the entries of l read backwards.

theorem TauCeti.Polynomial.eval₂_ofCoeffList {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] (f : R →+* S) (r : S) (l : List R) : Polynomial.eval₂ f r (ofCoeffList l) = List.foldl (fun (y : S) (a : R) => y * r + f a) 0 l

Evaluating TauCeti.Polynomial.ofCoeffList l is Horner's rule run directly on the list.

theorem TauCeti.Polynomial.degree_ofCoeffList_lt {R : Type u_1} [Semiring R] (l : List R) : (ofCoeffList l).degree < ↑l.length

A list of n coefficients defines a polynomial of degree less than n.

@[simp]

theorem TauCeti.Polynomial.ofCoeffList_cons {R : Type u_1} [Semiring R] (a : R) (l : List R) : ofCoeffList (a :: l) = Polynomial.C a * Polynomial.X ^ l.length + ofCoeffList l

Splitting off the leading coefficient of a list of coefficients.

theorem TauCeti.Polynomial.ofCoeffList_zero_cons {R : Type u_1} [Semiring R] (l : List R) : ofCoeffList (0 :: l) = ofCoeffList l

A leading zero coefficient may be dropped. This is not a simp lemma: simp already gets there through TauCeti.Polynomial.ofCoeffList_cons.

@[simp]

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

A list of zeros defines the zero polynomial.

theorem TauCeti.Polynomial.ofCoeffList_eq_headD_add_tail {R : Type u_1} [Semiring R] {l : List R} (hl : l ≠ []) : ofCoeffList l = Polynomial.C (l.headD 0) * Polynomial.X ^ l.tail.length + ofCoeffList l.tail

Splitting off the leading coefficient of a nonempty list of coefficients.

theorem TauCeti.Polynomial.coeff_ofCoeffList_length_sub_one {R : Type u_1} [Semiring R] (l : List R) : (ofCoeffList l).coeff (l.length - 1) = l.headD 0

The top coefficient of TauCeti.Polynomial.ofCoeffList l is the head of l.

theorem TauCeti.Polynomial.natDegree_ofCoeffList {R : Type u_1} [Semiring R] {l : List R} (h : l = [] ∨ l.headD 0 ≠ 0) : (ofCoeffList l).natDegree = l.length - 1

A list with no leading zero has exactly one more entry than the degree of the polynomial it defines. The empty list is allowed: it defines 0, of degree 0.

theorem TauCeti.Polynomial.leadingCoeff_ofCoeffList {R : Type u_1} [Semiring R] {l : List R} (h : l = [] ∨ l.headD 0 ≠ 0) : (ofCoeffList l).leadingCoeff = l.headD 0

A list with no leading zero has its head as the leading coefficient of the polynomial it defines. The empty list is allowed: it defines 0, whose leading coefficient is 0.

theorem TauCeti.Polynomial.eq_of_length_eq_of_ofCoeffList_eq {R : Type u_1} [Semiring R] {l l' : List R} (hlen : l.length = l'.length) (h : ofCoeffList l = ofCoeffList l') : l = l'

Two lists of the same length define the same polynomial only if they are equal. This is not injectivity of TauCeti.Polynomial.ofCoeffList, which discards leading zeros.

theorem TauCeti.Polynomial.coeffList_ofCoeffList {R : Type u_1} [Semiring R] {l : List R} (h : l = [] ∨ l.headD 0 ≠ 0) : (ofCoeffList l).coeffList = l

TauCeti.Polynomial.ofCoeffList inverts Mathlib's Polynomial.coeffList on the lists that arise as coefficient lists, namely those with no leading zero.

@[simp]

theorem TauCeti.Polynomial.ofCoeffList_coeffList {R : Type u_1} [Semiring R] (p : Polynomial R) : ofCoeffList p.coeffList = p

TauCeti.Polynomial.ofCoeffList is a left inverse of Mathlib's Polynomial.coeffList: every polynomial is recovered from its coefficient list.

def TauCeti.Polynomial.mulCoeffList {R : Type u_1} [Semiring R] (l m : List R) : List R

Multiplication of descending coefficient lists, by convolving them in ascending degree order. The output has the usual l.length + m.length - 1 slots; if either input is empty, all of those slots are zero. This is @[expose]d, since a consumer computing with it in another module reduces it in the kernel.

Equations

• TauCeti.Polynomial.mulCoeffList l m = (List.ofFn fun (i : Fin (l.length + m.length - 1)) => ∑ jk ∈ Finset.antidiagonal ↑i, l.reverse.getD jk.1 0 * m.reverse.getD jk.2 0).reverse

theorem TauCeti.Polynomial.ofCoeffList_mulCoeffList {R : Type u_1} [Semiring R] (l m : List R) : ofCoeffList (mulCoeffList l m) = ofCoeffList l * ofCoeffList m

TauCeti.Polynomial.mulCoeffList lists the coefficients of a product of polynomials.

theorem TauCeti.Polynomial.monic_X_pow_add_ofCoeffList {R : Type u_1} [Semiring R] (t : List R) : (Polynomial.X ^ t.length + ofCoeffList t).Monic

The divisor X ^ t.length + ofCoeffList t of TauCeti.Polynomial.divModByMonicList is monic.

theorem TauCeti.Polynomial.degree_X_pow_add_ofCoeffList {R : Type u_1} [Semiring R] [Nontrivial R] (t : List R) : (Polynomial.X ^ t.length + ofCoeffList t).degree = ↑t.length

The divisor X ^ t.length + ofCoeffList t has degree exactly t.length.

theorem TauCeti.Polynomial.X_pow_add_ofCoeffList_tail {R : Type u_1} [Semiring R] {l : List R} (hhead : l.headD 0 ≠ 0) (hmonic : (ofCoeffList l).Monic) : Polynomial.X ^ l.tail.length + ofCoeffList l.tail = ofCoeffList l

A monic polynomial is X ^ n plus the polynomial of its remaining coefficients. This is how a computed coefficient list is recognized as a divisor for TauCeti.Polynomial.divByMonicList.

@[simp]

theorem TauCeti.Polynomial.ofCoeffList_map_mul_left {R : Type u_1} [Semiring R] (c : R) (l : List R) : ofCoeffList (List.map (fun (x : R) => c * x) l) = Polynomial.C c * ofCoeffList l

Scaling every coefficient on the left scales the polynomial.

@[simp]

theorem TauCeti.Polynomial.ofCoeffList_map_neg {R : Type u_1} [Ring R] (l : List R) : ofCoeffList (List.map (fun (x : R) => -x) l) = -ofCoeffList l

Negating every coefficient negates the polynomial.

theorem TauCeti.Polynomial.ofCoeffList_zipWith_sub {R : Type u_1} [Ring R] (c : R) {l l' : List R} (h : l.length = l'.length) : ofCoeffList (List.zipWith (fun (x y : R) => x - y * c) l l') = ofCoeffList l - ofCoeffList l' * Polynomial.C c

Subtracting a right multiple of one list of coefficients from another, entrywise.

def TauCeti.Polynomial.divModByMonicStep {R : Type u_1} [Ring R] (t : List R) (qr : List R × List R) (a : R) : List R × List R

One step of synthetic division by the monic polynomial X ^ t.length + ofCoeffList t: the pair qr holds the quotient coefficients found so far together with a window of t.length remainder coefficients, and a is the next coefficient of the dividend.

Equations

• TauCeti.Polynomial.divModByMonicStep t qr a = (qr.1 ++ [(qr.2 ++ [a]).headD 0], List.zipWith (fun (x y : R) => x - y * (qr.2 ++ [a]).headD 0) (qr.2 ++ [a]).tail t)

@[simp]

theorem TauCeti.Polynomial.divModByMonicStep_fst {R : Type u_1} [Ring R] (t : List R) (qr : List R × List R) (a : R) : (divModByMonicStep t qr a).1 = qr.1 ++ [(qr.2 ++ [a]).headD 0]

One step of synthetic division appends the coefficient shifted out of the remainder window to the quotient.

@[simp]

theorem TauCeti.Polynomial.divModByMonicStep_snd {R : Type u_1} [Ring R] (t : List R) (qr : List R × List R) (a : R) : (divModByMonicStep t qr a).2 = List.zipWith (fun (x y : R) => x - y * (qr.2 ++ [a]).headD 0) (qr.2 ++ [a]).tail t

One step of synthetic division clears the remaining window against the divisor.

def TauCeti.Polynomial.divModByMonicList {R : Type u_1} [Ring R] (t l : List R) : List R × List R

Long division of the polynomial with coefficient list l by the monic polynomial X ^ t.length + ofCoeffList t, by synthetic division. The first component is the coefficient list of the quotient, the second that of the remainder.

Equations

• TauCeti.Polynomial.divModByMonicList t l = List.foldl (TauCeti.Polynomial.divModByMonicStep t) ([], List.replicate t.length 0) l

def TauCeti.Polynomial.divByMonicList {R : Type u_1} [Ring R] (t l : List R) : List R

The quotient of ofCoeffList l by the monic polynomial X ^ t.length + ofCoeffList t, as a coefficient list.

Equations

• TauCeti.Polynomial.divByMonicList t l = (TauCeti.Polynomial.divModByMonicList t l).1

def TauCeti.Polynomial.modByMonicList {R : Type u_1} [Ring R] (t l : List R) : List R

The remainder of ofCoeffList l on division by the monic polynomial X ^ t.length + ofCoeffList t, as a coefficient list.

Equations

• TauCeti.Polynomial.modByMonicList t l = (TauCeti.Polynomial.divModByMonicList t l).2

@[simp]

theorem TauCeti.Polynomial.divModByMonicList_nil {R : Type u_1} [Ring R] (t : List R) : divModByMonicList t [] = ([], List.replicate t.length 0)

Dividing the zero polynomial leaves the empty quotient and the zero remainder window.

@[simp]

theorem TauCeti.Polynomial.divModByMonicList_concat {R : Type u_1} [Ring R] (t l : List R) (a : R) : divModByMonicList t (l ++ [a]) = divModByMonicStep t (divModByMonicList t l) a

The division sweeps the dividend from the top coefficient down, one step per coefficient.

theorem TauCeti.Polynomial.length_divModByMonicList_snd {R : Type u_1} [Ring R] (t l : List R) : (divModByMonicList t l).2.length = t.length

The remainder window keeps the length of the divisor's degree throughout the division.

@[simp]

theorem TauCeti.Polynomial.length_modByMonicList {R : Type u_1} [Ring R] (t l : List R) : (modByMonicList t l).length = t.length

The computed remainder has the length of the divisor's degree.

theorem TauCeti.Polynomial.ofCoeffList_divModByMonicList {R : Type u_1} [Ring R] (t l : List R) : ofCoeffList l = (Polynomial.X ^ t.length + ofCoeffList t) * ofCoeffList (divModByMonicList t l).1 + ofCoeffList (divModByMonicList t l).2

The division identity for synthetic division: at every stage of the sweep, the part of the dividend read so far is the divisor times the quotient found so far, plus the remainder window.

@[simp]

theorem TauCeti.Polynomial.ofCoeffList_divByMonicList {R : Type u_1} [Ring R] (t l : List R) : ofCoeffList (divByMonicList t l) = ofCoeffList l /ₘ (Polynomial.X ^ t.length + ofCoeffList t)

Synthetic division computes the quotient: the first output of TauCeti.Polynomial.divModByMonicList is Mathlib's /ₘ by the monic divisor.

@[simp]

theorem TauCeti.Polynomial.ofCoeffList_modByMonicList {R : Type u_1} [Ring R] (t l : List R) : ofCoeffList (modByMonicList t l) = ofCoeffList l %ₘ (Polynomial.X ^ t.length + ofCoeffList t)

Synthetic division computes the remainder: the second output of TauCeti.Polynomial.divModByMonicList is Mathlib's %ₘ by the monic divisor.