Executable exact rational polynomials

Polynomial ℚ is the semantic representation used by Mathlib, but its sparse implementation is not a suitable native certificate payload. QPoly stores ascending coefficients in an Array ℚ and supplies a small exact executable kernel. The toPoly lemmas connect successful computations to Mathlib.

structure LeanCert.Engine.QPoly : Type

An exact executable rational polynomial.

coeffs[i] is the coefficient of x^i. Trailing zero coefficients are allowed; use trim when a canonical certificate representation is useful.

• coeffs : Array ℚ

def LeanCert.Engine.instDecidableEqQPoly.decEq (x✝ x✝¹ : QPoly) : Decidable (x✝ = x✝¹)

Equations

• LeanCert.Engine.instDecidableEqQPoly.decEq { coeffs := a } { coeffs := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance LeanCert.Engine.instDecidableEqQPoly : DecidableEq QPoly

Equations

• LeanCert.Engine.instDecidableEqQPoly = LeanCert.Engine.instDecidableEqQPoly.decEq

def LeanCert.Engine.instReprQPoly.repr : QPoly → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance LeanCert.Engine.instReprQPoly : Repr QPoly

Equations

• LeanCert.Engine.instReprQPoly = { reprPrec := LeanCert.Engine.instReprQPoly.repr }

@[instance_reducible]

instance LeanCert.Engine.instInhabitedQPoly : Inhabited QPoly

Equations

• LeanCert.Engine.instInhabitedQPoly = { default := LeanCert.Engine.instInhabitedQPoly.default }

noncomputable def LeanCert.Engine.QPoly.toPoly (p : QPoly) : Polynomial ℚ

The semantic Mathlib polynomial represented by an executable QPoly.

Equations

• p.toPoly = LeanCert.Engine.QPoly.listToPoly✝ p.coeffs.toList

def LeanCert.Engine.QPoly.zero : QPoly

Equations

• LeanCert.Engine.QPoly.zero = { coeffs := #[] }

def LeanCert.Engine.QPoly.constant (c : ℚ) : QPoly

Equations

• LeanCert.Engine.QPoly.constant c = { coeffs := #[c] }

def LeanCert.Engine.QPoly.X : QPoly

The polynomial variable.

Equations

• LeanCert.Engine.QPoly.X = { coeffs := #[0, 1] }

def LeanCert.Engine.QPoly.add (p q : QPoly) : QPoly

Equations

• p.add q = { coeffs := (LeanCert.Engine.QPoly.addCoeffs✝ p.coeffs.toList q.coeffs.toList).toArray }

def LeanCert.Engine.QPoly.mul (p q : QPoly) : QPoly

Equations

• p.mul q = { coeffs := (LeanCert.Engine.QPoly.mulCoeffs✝ p.coeffs.toList q.coeffs.toList).toArray }

def LeanCert.Engine.QPoly.derivative (p : QPoly) : QPoly

Equations

• p.derivative = { coeffs := (LeanCert.Engine.QPoly.trimCoeffs✝ (LeanCert.Engine.QPoly.derivativeCoeffs✝ p.coeffs.toList)).toArray }

def LeanCert.Engine.QPoly.antiderivative (p : QPoly) : QPoly

The exact rational antiderivative with constant coefficient zero.

Equations

• p.antiderivative = { coeffs := (0 :: LeanCert.Engine.QPoly.antiderivativeCoeffs✝ 1 p.coeffs.toList).toArray }

def LeanCert.Engine.QPoly.evalRat (p : QPoly) (x : ℚ) : ℚ

Exact Horner evaluation over the rationals.

Equations

• p.evalRat x = LeanCert.Engine.QPoly.evalCoeffs✝ x p.coeffs.toList

def LeanCert.Engine.QPoly.integralRat (p : QPoly) (a b : ℚ) : ℚ

Exact definite integral between rational endpoints.

Equations

• p.integralRat a b = p.antiderivative.evalRat b - p.antiderivative.evalRat a

def LeanCert.Engine.QPoly.trim (p : QPoly) : QPoly

Equations

• p.trim = { coeffs := (LeanCert.Engine.QPoly.trimCoeffs✝ p.coeffs.toList).toArray }

@[simp]

theorem LeanCert.Engine.QPoly.toPoly_zero : zero.toPoly = 0

@[simp]

theorem LeanCert.Engine.QPoly.toPoly_constant (c : ℚ) : (constant c).toPoly = Polynomial.C c

@[simp]

theorem LeanCert.Engine.QPoly.toPoly_X : X.toPoly = Polynomial.X

theorem LeanCert.Engine.QPoly.toPoly_add (p q : QPoly) : (p.add q).toPoly = p.toPoly + q.toPoly

theorem LeanCert.Engine.QPoly.toPoly_mul (p q : QPoly) : (p.mul q).toPoly = p.toPoly * q.toPoly

theorem LeanCert.Engine.QPoly.toPoly_derivative (p : QPoly) : p.derivative.toPoly = Polynomial.derivative p.toPoly

theorem LeanCert.Engine.QPoly.toPoly_antiderivative_derivative (p : QPoly) : Polynomial.derivative p.antiderivative.toPoly = p.toPoly

theorem LeanCert.Engine.QPoly.toPoly_trim (p : QPoly) : p.trim.toPoly = p.toPoly

Sparse products with 1 - X^n and monomial shifts

mul is dense (O(deg p · deg q)), which is far too slow for products of a few hundred factors 1 - X^n of total degree in the hundreds of thousands. mulOneSubPow computes p · (1 - X^n) as p - X^n · p in linear time.

def LeanCert.Engine.QPoly.shiftPow (p : QPoly) (k : ℕ) : QPoly

X^k · p, in linear time.

Equations

• p.shiftPow k = { coeffs := (List.replicate k 0 ++ p.coeffs.toList).toArray }

theorem LeanCert.Engine.QPoly.toPoly_shiftPow (p : QPoly) (k : ℕ) : (p.shiftPow k).toPoly = Polynomial.X ^ k * p.toPoly

def LeanCert.Engine.QPoly.mulOneSubPow (p : QPoly) (n : ℕ) : QPoly

p · (1 - X^n), in linear time.

Equations

• p.mulOneSubPow n = { coeffs := (LeanCert.Engine.QPoly.addCoeffs✝ p.coeffs.toList (List.replicate n 0 ++ LeanCert.Engine.QPoly.negCoeffs✝ p.coeffs.toList)).toArray }

theorem LeanCert.Engine.QPoly.toPoly_mulOneSubPow (p : QPoly) (n : ℕ) : (p.mulOneSubPow n).toPoly = p.toPoly * (1 - Polynomial.X ^ n)

Composition and coefficient sums

def LeanCert.Engine.QPoly.compose (p q : QPoly) : QPoly

Horner composition p ∘ q, exact over the rationals.

Equations

• p.compose q = LeanCert.Engine.QPoly.composeCoeffs✝ q p.coeffs.toList

theorem LeanCert.Engine.QPoly.toPoly_compose (p q : QPoly) : (p.compose q).toPoly = p.toPoly.comp q.toPoly

theorem LeanCert.Engine.QPoly.aeval_compose (p q : QPoly) (x : ℝ) : (Polynomial.aeval x) (p.compose q).toPoly = (Polynomial.aeval ((Polynomial.aeval x) q.toPoly)) p.toPoly

Evaluating a composition evaluates the inner polynomial first.

theorem LeanCert.Engine.QPoly.aeval_toPoly_eq_sum (p : QPoly) (x : ℝ) : (Polynomial.aeval x) p.toPoly = ∑ j ∈ Finset.range p.coeffs.toList.length, ↑(p.coeffs.toList.getD j 0) * x ^ j

The represented polynomial is the finite sum of its coefficient list.

def LeanCert.Engine.QPoly.toExpr (p : QPoly) : Core.Expr

Convert to a single-variable Horner expression in variable 0.

Equations

• p.toExpr = LeanCert.Engine.QPoly.listToExpr✝ p.coeffs.toList

theorem LeanCert.Engine.QPoly.eval_toExpr (p : QPoly) (x : ℝ) : Core.Expr.eval (fun (x_1 : ℕ) => x) p.toExpr = (Polynomial.aeval x) p.toPoly

The Horner Expr and Mathlib polynomial have identical real semantics.

theorem LeanCert.Engine.QPoly.cast_evalRat (p : QPoly) (x : ℚ) : ↑(p.evalRat x) = Core.Expr.eval (fun (x_1 : ℕ) => ↑x) p.toExpr

theorem LeanCert.Engine.QPoly.integral_eval_toExpr (p : QPoly) (a b : ℚ) : ∫ (x : ℝ) in ↑a..↑b, Core.Expr.eval (fun (x_1 : ℕ) => x) p.toExpr = ↑(p.integralRat a b)

The executable exact integral agrees with the interval integral of the represented polynomial.

theorem LeanCert.Engine.QPoly.deriv_eval_toExpr (p : QPoly) (x : ℝ) : deriv (fun (t : ℝ) => Core.Expr.eval (fun (x : ℕ) => t) p.toExpr) x = (Polynomial.aeval x) (Polynomial.derivative p.toPoly)

The analytic derivative of the Horner expression agrees with the formal polynomial derivative.