noncomputable def HexPolyTheory.polynomialOfList : List ℚ → Polynomial ℚ

A polynomial represented by an ascending coefficient list.

Equations

• HexPolyTheory.polynomialOfList [] = 0
• HexPolyTheory.polynomialOfList (a :: as) = Polynomial.C a + Polynomial.X * HexPolyTheory.polynomialOfList as

theorem HexPolyTheory.polynomialOfList_coeff (xs : List ℚ) (i : ℕ) : (polynomialOfList xs).coeff i = xs.getD i 0

theorem HexPolyTheory.polynomialOfList_eq (xs : List ℚ) : polynomialOfList xs = toPolynomial (Hex.DensePoly.ofList xs)

def HexPolyTheory.addLists : List ℚ → List ℚ → List ℚ

Addition on ascending coefficients, preserving zeros for cheap reduction.

Equations

• HexPolyTheory.addLists [] x✝ = x✝
• HexPolyTheory.addLists x✝ [] = x✝
• HexPolyTheory.addLists (x_2 :: xs) (y :: ys) = x_2.add y :: HexPolyTheory.addLists xs ys

def HexPolyTheory.scaleList (a : ℚ) (xs : List ℚ) : List ℚ

Scale ascending coefficients.

Equations

• HexPolyTheory.scaleList a xs = List.map a.mul xs

def HexPolyTheory.mulLists : List ℚ → List ℚ → List ℚ

Structural coefficient convolution.

Equations

• HexPolyTheory.mulLists [] x✝ = []
• HexPolyTheory.mulLists (x_2 :: xs) x✝ = HexPolyTheory.addLists (HexPolyTheory.scaleList x_2 x✝) (0 :: HexPolyTheory.mulLists xs x✝)

theorem HexPolyTheory.polynomialOfList_add (xs ys : List ℚ) : polynomialOfList (addLists xs ys) = polynomialOfList xs + polynomialOfList ys

theorem HexPolyTheory.polynomialOfList_scale (a : ℚ) (xs : List ℚ) : polynomialOfList (scaleList a xs) = Polynomial.C a * polynomialOfList xs

theorem HexPolyTheory.polynomialOfList_mul (xs ys : List ℚ) : polynomialOfList (mulLists xs ys) = polynomialOfList xs * polynomialOfList ys

theorem HexPolyTheory.polynomialOfList_X : polynomialOfList [0, 1] = Polynomial.X

theorem HexPolyTheory.polynomialOfList_C (a : ℚ) : polynomialOfList [a] = Polynomial.C a

theorem HexPolyTheory.polynomialOfList_neg (xs : List ℚ) : polynomialOfList (scaleList (-1) xs) = -polynomialOfList xs

def HexPolyTheory.powList (xs : List ℚ) : ℕ → List ℚ

Equations

• HexPolyTheory.powList xs 0 = [1]
• HexPolyTheory.powList xs n.succ = HexPolyTheory.mulLists (HexPolyTheory.powList xs n) xs

theorem HexPolyTheory.polynomialOfList_pow (xs : List ℚ) (n : ℕ) : polynomialOfList (powList xs n) = polynomialOfList xs ^ n

theorem HexPolyTheory.polynomialOfList_nat (n : ℕ) : polynomialOfList [↑n] = ↑n

theorem HexPolyTheory.polynomialOfList_zero : 0 = polynomialOfList [0]

theorem HexPolyTheory.polynomialOfList_one : 1 = polynomialOfList [1]

theorem HexPolyTheory.polynomialOfList_sub (xs ys : List ℚ) : polynomialOfList (addLists xs (scaleList (-1) ys)) = polynomialOfList xs - polynomialOfList ys