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.

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₂Horner {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 Horner's method.

Computes f(aₙ) + x * (f(aₙ₋₁) + x * (... + x * f(a₀))) via a right fold.

Equations

• CompPoly.CPolynomial.Raw.eval₂Horner f x p = Array.foldr (fun (a : R) (acc : S) => acc * x + f a) 0 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.smulRight {R : Type u_1} [Mul R] (r : R) (p : Raw R) : Raw R

Right scalar multiplication: multiplies each coefficient by r on the right.

Corresponds to p.toPoly * Polynomial.C r, in contrast to smul which corresponds to Polynomial.C r * p.toPoly. The distinction matters in non-commutative semirings.

Equations

• CompPoly.CPolynomial.Raw.smulRight r p = CompPoly.CPolynomial.Raw.mk (Array.map (fun (a : R) => a * r) 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.mulRaw {R : Type u_1} [Semiring R] (p q : Raw R) : Raw R

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

The partial sums are combined with the untrimmed addRaw, so the result may carry trailing zeros and should be trimmed for canonical form. Deferring the trim to the end (see mul) avoids an O(size) scan after every partial sum.

Equations

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

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

Trims only once, at the end of the convolution fold, rather than after every partial sum (mulRaw does the untrimmed accumulation).

Equations

• p.mul q = (p.mulRaw q).trim

@[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.powBySqUntrimmed {R : Type u_1} [Semiring R] (p : Raw R) : ℕ → Raw R

Repeated-squaring core that accumulates with the untrimmed mulRaw, deferring the canonicalization trim to the outer powBySq wrapper. The output may carry trailing zeros and is not in canonical form.

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

• One or more equations did not get rendered due to their size.
• p.powBySqUntrimmed 0 = CompPoly.CPolynomial.Raw.C 1

@[inline, specialize #[]]

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

Exponentiation via repeated squaring: $ O(\log n) $ multiplications instead of $ O(n) $. Delegates to powBySqUntrimmed and trims only once at the end, rather than after every squaring step.

Equations

• p.powBySq n = (p.powBySqUntrimmed n).trim

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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_reducible]

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_reducible]

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_reducible]

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_reducible]

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_reducible]

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_reducible]

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 }

@[inline, specialize #[]]

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

Keep only the stored coefficients with index < k.

Equations

• CompPoly.CPolynomial.Raw.truncate k p = Array.extract p 0 k

@[inline, specialize #[]]

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

Return exactly the first k coefficients, padding missing coefficients with zero.

Equations

• CompPoly.CPolynomial.Raw.takeLow k p = Array.ofFn fun (i : Fin k) => p.coeff ↑i

@[inline, specialize #[]]

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

Reverse the first n coefficients, padding missing coefficients with zero.

Equations

• CompPoly.CPolynomial.Raw.reverse n p = Array.ofFn fun (i : Fin n) => p.coeff (n - 1 - ↑i)

@[inline, specialize #[]]

def CompPoly.CPolynomial.Raw.mulLowConvolution {R : Type u_1} [Semiring R] (k : ℕ) (p q : Raw R) : Raw R

Low product computed by the coefficient convolution formula.

Equations

• CompPoly.CPolynomial.Raw.mulLowConvolution k p q = Array.ofFn fun (i : Fin k) => ∑ j ∈ Finset.range (↑i + 1), p.coeff j * q.coeff (↑i - j)

structure CompPoly.CPolynomial.Raw.MulLowContext (R : Type u_4) [Semiring R] [BEq R] [LawfulBEq R] : Type u_4

Backend for computing the low k coefficients of a raw product.

• mulLow : ℕ → Raw R → Raw R → Raw R

  Return the low k coefficients of p * q.

• size_le (k : ℕ) (p q : Raw R) : Array.size (self.mulLow k p q) ≤ k

  The backend does not return coefficients at degree >= k.

• coeff_of_lt (k : ℕ) (p q : Raw R) (i : ℕ) : i < k → (self.mulLow k p q).coeff i = (p * q).coeff i

  Low coefficients agree with ordinary raw multiplication.

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_reducible]

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_reducible]

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_reducible]

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 }