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

Equations

• CompPoly.CPolynomial.Raw.eval₂ f x p = Array.foldl (fun (acc : S) (x_1 : R × ℕ) => match x_1 with | (a, i) => acc + f a * x ^ i) 0 (Array.zipIdx p)

@[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

Equations

• CompPoly.CPolynomial.Raw.eval x p = CompPoly.CPolynomial.Raw.eval₂ (RingHom.id R) x p

@[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.

Equations

• p.addRaw q = match Array.matchSize p q 0 with | (p', q') => CompPoly.CPolynomial.Raw.mk (Array.zipWith (fun (x1 x2 : R) => x1 + x2) p' q')

@[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.

Equations

• p.add q = (p.addRaw q).trim

@[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.

Equations

• CompPoly.CPolynomial.Raw.smul r p = CompPoly.CPolynomial.Raw.mk (Array.map (fun (a : R) => r * a) p)

@[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).

Equations

• CompPoly.CPolynomial.Raw.nsmulRaw n p = CompPoly.CPolynomial.Raw.mk (Array.map (fun (a : R) => ↑n * a) p)

@[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.

Equations

• CompPoly.CPolynomial.Raw.nsmul n p = (CompPoly.CPolynomial.Raw.nsmulRaw n p).trim

@[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).

Equations

• CompPoly.CPolynomial.Raw.mulPowX i p = CompPoly.CPolynomial.Raw.mk (Array.replicate i 0 ++ p)

@[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.

Equations

• p.mulX = CompPoly.CPolynomial.Raw.mulPowX 1 p

@[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.

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• p.pow n = p.mul^[n] (CompPoly.CPolynomial.Raw.C 1)

@[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 $

Equations

• p.powBySq 0 = CompPoly.CPolynomial.Raw.C 1
• p.powBySq n.succ = if (n + 1) % 2 = 0 then (p.powBySq ((n + 1) / 2)).mul (p.powBySq ((n + 1) / 2)) else p.mul ((p.powBySq ((n + 1) / 2)).mul (p.powBySq ((n + 1) / 2)))

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

Equations

• CompPoly.CPolynomial.Raw.instZero = { zero := #[] }

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

Equations

• CompPoly.CPolynomial.Raw.instOne = { one := CompPoly.CPolynomial.Raw.C 1 }

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

Equations

• CompPoly.CPolynomial.Raw.instAddOfZeroOfBEq = { add := CompPoly.CPolynomial.Raw.add }

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

Equations

• CompPoly.CPolynomial.Raw.instSMulOfMul = { smul := CompPoly.CPolynomial.Raw.smul }

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

Equations

• CompPoly.CPolynomial.Raw.instSMulNatOfSemiringOfBEq = { smul := CompPoly.CPolynomial.Raw.nsmul }

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

Equations

• CompPoly.CPolynomial.Raw.instMulOfSemiringOfBEq = { mul := CompPoly.CPolynomial.Raw.mul }

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

Equations

• CompPoly.CPolynomial.Raw.instPowNatOfSemiringOfBEq = { pow := CompPoly.CPolynomial.Raw.pow }

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

Equations

• CompPoly.CPolynomial.Raw.instNatCast = { natCast := fun (n : ℕ) => CompPoly.CPolynomial.Raw.C ↑n }

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

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

Equations

• p.degreeBound = match Array.size p with | 0 => ⊥ | n.succ => ↑n

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

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

Equations

• p.natDegreeBound = Option.getD p.degreeBound 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.

Equations

• p.monic = (p.leadingCoeff == 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.

Equations

• p.divX = Array.extract p 1

@[inline, specialize #[]]

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

Negation of a CPolynomial.Raw.

Equations

• p.neg = Array.map (fun (a : R) => -a) p

@[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.

Equations

• p.sub q = p.add q.neg

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

Equations

• CompPoly.CPolynomial.Raw.instNeg = { neg := CompPoly.CPolynomial.Raw.neg }

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

Equations

• CompPoly.CPolynomial.Raw.instSubOfZeroOfAddOfNegOfBEq = { sub := CompPoly.CPolynomial.Raw.sub }

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

Equations

• CompPoly.CPolynomial.Raw.instIntCast = { intCast := fun (n : ℤ) => CompPoly.CPolynomial.Raw.C ↑n }

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.

Equations

• CompPoly.CPolynomial.Raw.erase n p = p - CompPoly.CPolynomial.Raw.monomial n (p.coeff n)