Computable Univariate To Polynomial

Conversions between computable univariate polynomials and mathlib Polynomial.

def Polynomial.toImpl {R : Type u_1} [Semiring R] (p : Polynomial R) : CompPoly.CPolynomial.Raw R

Convert a mathlib Polynomial to a CPolynomial.Raw by extracting coefficients up to the degree.

Equations

• p.toImpl = match p.degree with | none => #[] | some d => Array.ofFn fun (i : Fin (d + 1)) => p.coeff ↑i

noncomputable def CompPoly.CPolynomial.Raw.toPoly {R : Type u_1} [Semiring R] (p : Raw R) : Polynomial R

Convert a CPolynomial.Raw to a (mathlib) Polynomial.

Equations

• p.toPoly = CompPoly.CPolynomial.Raw.eval₂ Polynomial.C Polynomial.X p

noncomputable def CompPoly.CPolynomial.Raw.toPoly' {R : Type u_1} [Semiring R] (p : Raw R) : Polynomial R

Alternative definition of toPoly using Finsupp; currently unused.

Equations

• p.toPoly' = { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.onFinset (Finset.range (Array.size p)) p.coeff ⋯) }

noncomputable def CompPoly.CPolynomial.toPoly {R : Type u_1} [Semiring R] (p : CPolynomial R) : Polynomial R

Convert a canonical polynomial to a (mathlib) Polynomial.

Equations

• p.toPoly = (↑p).toPoly

def CompPoly.CPolynomial.Raw.ofPoly {R : Type u_1} [Semiring R] (p : Polynomial R) : Raw R

Alias of Polynomial.toImpl.

---

Convert a mathlib Polynomial to a CPolynomial.Raw by extracting coefficients up to the degree.

Equations

• @CompPoly.CPolynomial.Raw.ofPoly = @Polynomial.toImpl

theorem CompPoly.CPolynomial.Raw.eval_toPoly_eq_eval {Q : Type u_2} [Semiring Q] (x : Q) (p : Raw Q) : Polynomial.eval x p.toPoly = eval x p

Evaluation is preserved by toPoly.

theorem CompPoly.CPolynomial.Raw.coeff_toPoly {Q : Type u_2} [Semiring Q] {p : Raw Q} {n : ℕ} : p.toPoly.coeff n = p.coeff n

The coefficients of p.toPoly match those of p.

theorem CompPoly.CPolynomial.Raw.toImpl_elim {Q : Type u_2} [Semiring Q] (p : Polynomial Q) : p = 0 ∧ p.toImpl = #[] ∨ p ≠ 0 ∧ p.toImpl = Array.ofFn fun (i : Fin (p.natDegree + 1)) => p.coeff ↑i

Case analysis for toImpl: either the polynomial is zero or has a specific form.

theorem CompPoly.CPolynomial.Raw.toPoly_toImpl {Q : Type u_2} [Semiring Q] {p : Polynomial Q} : p.toImpl.toPoly = p

toImpl is a right-inverse of toPoly: the round-trip from Polynomial is the identity.

This shows toPoly is surjective and toImpl is injective.

theorem CompPoly.CPolynomial.Raw.toPoly_trim {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] {p : Raw R} : p.trim.toPoly = p.toPoly

Trimming doesn't change the toPoly image.

theorem CompPoly.CPolynomial.Raw.toPoly_addRaw {Q : Type u_2} [Semiring Q] {p q : Raw Q} : (p.addRaw q).toPoly = p.toPoly + q.toPoly

toPoly preserves addition.

theorem CompPoly.CPolynomial.Raw.toPoly_smulRight {Q : Type u_2} [Semiring Q] {p : Raw Q} {r : Q} : (smulRight r p).toPoly = p.toPoly * Polynomial.C r

toPoly of a right-scalar multiplication is multiplication by Polynomial.C r on the right.

theorem CompPoly.CPolynomial.Raw.toPoly_add {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q : Raw R) : (p + q).toPoly = p.toPoly + q.toPoly

theorem CompPoly.CPolynomial.Raw.toImpl_nonzero {Q : Type u_2} [Semiring Q] {p : Polynomial Q} (hp : p ≠ 0) : Array.size p.toImpl > 0

Non-zero polynomials map to non-empty arrays.

theorem CompPoly.CPolynomial.Raw.getLast_toImpl {Q : Type u_2} [Semiring Q] {p : Polynomial Q} (hp : p ≠ 0) : have h := ⋯; p.toImpl[Array.size p.toImpl - 1] = p.leadingCoeff

The last coefficient of toImpl p is the leading coefficient of p.

@[simp]

theorem CompPoly.CPolynomial.Raw.isCanonical_toImpl {R : Type u_1} [Semiring R] (p : Polynomial R) : p.toImpl.IsCanonical

toImpl lands in the semantic canonical carrier used by CPolynomial.

@[simp]

theorem CompPoly.CPolynomial.Raw.trim_toImpl {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : Polynomial R) : p.toImpl.trim = p.toImpl

toImpl produces canonical polynomials (no trailing zeros).

theorem CompPoly.CPolynomial.toPoly_mk_toImpl {R : Type u_1} [Semiring R] (p : Polynomial R) : toPoly ⟨p.toImpl, ⋯⟩ = p

Building a canonical polynomial from toImpl and converting it back yields the original mathlib polynomial.

theorem CompPoly.CPolynomial.ofArray_toPoly {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : Raw R) : (ofArray p).toPoly = p.toPoly

ofArray preserves the raw polynomial's toPoly image.

theorem CompPoly.CPolynomial.toImpl_toPoly_of_canonical {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : p.toPoly.toImpl = ↑p

On canonical polynomials, toImpl is a left-inverse of toPoly.

This shows toPoly is a bijection from CPolynomial R to Polynomial R.

@[simp]

theorem CompPoly.CPolynomial.Raw.toImpl_toPoly {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : Raw R) : p.toPoly.toImpl = p.trim

The round-trip from CPolynomial.Raw to Polynomial and back yields the canonical form.

theorem CompPoly.CPolynomial.Raw.toPoly_natDegree_lt_trim_size_of_pos {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : Raw R) (hp : 0 < Array.size p.trim) : p.toPoly.natDegree < Array.size p.trim

A nonempty trimmed raw polynomial bounds the degree of its toPoly image.

theorem CompPoly.CPolynomial.toPoly_eq_zero_iff {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : p.toPoly = 0 ↔ p = 0

toPoly maps a canonical polynomial to 0 iff the polynomial is 0.

@[simp]

theorem CompPoly.CPolynomial.eval_toImpl_eq_eval {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (x : R) (p : Polynomial R) : Raw.eval x p.toImpl = Polynomial.eval x p

Evaluation is preserved by toImpl.

@[simp]

theorem CompPoly.CPolynomial.Raw.eval_trim_eq_eval {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (x : R) (p : Raw R) : eval x p.trim = eval x p

Evaluation is unchanged by trimming.