Raw Univariate Polynomial Operations

Operations and evaluation lemmas for raw computable univariate polynomials.

def CompPoly.CPolynomial.Raw.eval₂ {R : Type u_1} {S : Type u_3} [Semiring R] [Semiring S] (f : R →+* S) (x : S) (p : Raw R) : S

Evaluates a CPolynomial.Raw at x : S using a ring homomorphism f : R →+* S.

Computes f(a₀) + f(a₁) * x + f(a₂) * x² + ... where aᵢ are the coefficients.

TODO: define an efficient version of this with caching

@[inline, specialize #[]]

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

Evaluates a CPolynomial.Raw at a given value

@[inline, specialize #[]]

def CompPoly.CPolynomial.Raw.addRaw {R : Type u_1} [Zero R] [Add R] (p q : Raw R) : Raw R

Raw addition: pointwise sum of coefficient arrays (padded to equal length).

The result may have trailing zeros and should be trimmed for canonical form.

@[inline, specialize #[]]

def CompPoly.CPolynomial.Raw.add {R : Type u_1} [Zero R] [Add R] [BEq R] (p q : Raw R) : Raw R

Addition of two CPolynomial.Raws, with result trimmed.

@[inline, specialize #[]]

def CompPoly.CPolynomial.Raw.smul {R : Type u_1} [Mul R] (r : R) (p : Raw R) : Raw R

Scalar multiplication: multiplies each coefficient by r.

@[inline, specialize #[]]

def CompPoly.CPolynomial.Raw.nsmulRaw {R : Type u_1} [Semiring R] (n : ℕ) (p : Raw R) : Raw R

Raw scalar multiplication by a natural number (may have trailing zeros).

@[inline, specialize #[]]

def CompPoly.CPolynomial.Raw.nsmul {R : Type u_1} [Semiring R] [BEq R] (n : ℕ) (p : Raw R) : Raw R

Scalar multiplication of CPolynomial.Raw by a natural number, with result trimmed.

@[inline, specialize #[]]

def CompPoly.CPolynomial.Raw.mulPowX {R : Type u_1} [Zero R] (i : ℕ) (p : Raw R) : Raw R

Multiplication by X^i: shifts coefficients right by i positions (prepends i zeros).

@[inline, specialize #[]]

def CompPoly.CPolynomial.Raw.mulX {R : Type u_1} [Zero R] (p : Raw R) : Raw R

Multiplication of a CPolynomial.Raw by X, reduces to mulPowX 1.

@[inline, specialize #[]]

def CompPoly.CPolynomial.Raw.mul {R : Type u_1} [Semiring R] [BEq R] (p q : Raw R) : Raw R

Multiplication using the naive O(n²) algorithm: Σᵢ (aᵢ * q) * X^i.

@[inline, specialize #[]]

def CompPoly.CPolynomial.Raw.pow {R : Type u_1} [Semiring R] [BEq R] (p : Raw R) (n : ℕ) : Raw R

Exponentiation of a CPolynomial.Raw by a natural number n via repeated multiplication. This is the specification; powBySq is the efficient O(log n) implementation.

@[irreducible, inline, specialize #[]]

def CompPoly.CPolynomial.Raw.powBySq {R : Type u_1} [Semiring R] [BEq R] (p : Raw R) : ℕ → Raw R

Exponentiation via repeated squaring: $ O(\log n) $ multiplications instead of $ O(n) $.

For $ n > 0 $, computes $ p ^ n $ by recursing on $ n / 2 $:

• If $ n $ is even: $ (p ^ {n/2})^2 $
• If $ n $ is odd: $ p \cdot (p ^ {n/2})^2 $

@[implicit_reducible]

instance CompPoly.CPolynomial.Raw.instZero {R : Type u_1} : Zero (Raw R)

@[implicit_reducible]

instance CompPoly.CPolynomial.Raw.instOne {R : Type u_1} [One R] : One (Raw R)

@[implicit_reducible]

instance CompPoly.CPolynomial.Raw.instAddOfZeroOfBEq {R : Type u_1} [Zero R] [Add R] [BEq R] : Add (Raw R)

@[implicit_reducible]

instance CompPoly.CPolynomial.Raw.instSMulOfMul {R : Type u_1} [Mul R] : SMul R (Raw R)

@[implicit_reducible]

instance CompPoly.CPolynomial.Raw.instSMulNatOfSemiringOfBEq {R : Type u_1} [Semiring R] [BEq R] : SMul ℕ (Raw R)

@[implicit_reducible]

instance CompPoly.CPolynomial.Raw.instMulOfSemiringOfBEq {R : Type u_1} [Semiring R] [BEq R] : Mul (Raw R)

@[implicit_reducible]

instance CompPoly.CPolynomial.Raw.instPowNatOfSemiringOfBEq {R : Type u_1} [Semiring R] [BEq R] : Pow (Raw R) ℕ

@[implicit_reducible]

instance CompPoly.CPolynomial.Raw.instNatCast {R : Type u_1} [NatCast R] : NatCast (Raw R)

def CompPoly.CPolynomial.Raw.degreeBound {R : Type u_1} (p : Raw R) : WithBot ℕ

Upper bound on degree: size - 1 if non-empty, ⊥ if empty.

def CompPoly.CPolynomial.Raw.natDegreeBound {R : Type u_1} (p : Raw R) : ℕ

Convert degreeBound to a natural number by sending ⊥ to 0.

def CompPoly.CPolynomial.Raw.monic {R : Type u_1} [Zero R] [One R] [BEq R] (p : Raw R) : Bool

Check if a CPolynomial.Raw is monic, i.e. its leading coefficient is 1.

def CompPoly.CPolynomial.Raw.divX {R : Type u_1} (p : Raw R) : Raw R

Pseudo-division by X: removes the constant term and shifts remaining coefficients left.

@[inline, specialize #[]]

def CompPoly.CPolynomial.Raw.neg {R : Type u_1} [Neg R] (p : Raw R) : Raw R

Negation of a CPolynomial.Raw.

@[inline, specialize #[]]

def CompPoly.CPolynomial.Raw.sub {R : Type u_1} [Zero R] [Add R] [Neg R] [BEq R] (p q : Raw R) : Raw R

Subtraction of two CPolynomial.Raws.

@[implicit_reducible]

instance CompPoly.CPolynomial.Raw.instNeg {R : Type u_1} [Neg R] : Neg (Raw R)

@[implicit_reducible]

instance CompPoly.CPolynomial.Raw.instSubOfZeroOfAddOfNegOfBEq {R : Type u_1} [Zero R] [Add R] [Neg R] [BEq R] : Sub (Raw R)

@[implicit_reducible]

instance CompPoly.CPolynomial.Raw.instIntCast {R : Type u_1} [IntCast R] : IntCast (Raw R)

def CompPoly.CPolynomial.Raw.erase {R : Type u_1} [Zero R] [Add R] [Neg R] [BEq R] [DecidableEq R] (n : ℕ) (p : Raw R) : Raw R

Erase the coefficient at index n: same as p except coeff n = 0, then trimmed.