Documentation

CompPoly.Univariate.Deriv

Formal Derivative and Taylor Shift of Computable Univariate Polynomials #

Defines the formal derivative CPolynomial.derivative and the Taylor shift CPolynomial.taylor, with proofs of their core properties.

source
def CompPoly.CPolynomial.derivative {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) :
CPolynomial R

The formal derivative of a computable polynomial. Coefficient n of the result is coeff p (n+1) * (n+1).

Instances For
    source
    theorem CompPoly.CPolynomial.coeff_derivative {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) (n : ℕ) :
    p.derivative.coeff n = p.coeff (n + 1) * ↑(n + 1)

    Coefficient formula for the derivative.

    source
    theorem CompPoly.CPolynomial.derivative_zero {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] :
    derivative 0 = 0

    The derivative of the zero polynomial is zero.

    source
    theorem CompPoly.CPolynomial.derivative_C {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (r : R) :
    (C r).derivative = 0

    The derivative of a constant is zero.

    source
    theorem CompPoly.CPolynomial.derivative_monomial {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] (n : ℕ) (r : R) :
    (monomial n r).derivative = monomial (n - 1) (r * ↑n)

    The derivative of a monomial.

    source
    theorem CompPoly.CPolynomial.derivative_add {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] (p q : CPolynomial R) :
    (p + q).derivative = p.derivative + q.derivative

    The derivative distributes over addition.

    source
    theorem CompPoly.CPolynomial.derivative_toPoly {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) :
    p.derivative.toPoly = Polynomial.derivative p.toPoly

    The computable derivative matches Mathlib's Polynomial.derivative under toPoly.

    source
    theorem CompPoly.CPolynomial.derivative_mul {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p q : CPolynomial R) :
    (p * q).derivative = p.derivative * q + p * q.derivative

    The derivative satisfies the Leibniz product rule.

    source
    def CompPoly.CPolynomial.taylor {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (a : R) (p : CPolynomial R) :
    CPolynomial R

    The Taylor shift taylor a p = p(X + a).

    Instances For
      source
      theorem CompPoly.CPolynomial.taylor_toPoly {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (a : R) (p : CPolynomial R) :
      (taylor a p).toPoly = (Polynomial.taylor a) p.toPoly

      The computable Taylor shift matches Polynomial.taylor under toPoly.

      source
      theorem CompPoly.CPolynomial.taylor_zero {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (a : R) :
      taylor a 0 = 0

      The Taylor shift of zero is zero.

      source
      theorem CompPoly.CPolynomial.taylor_coeff_zero {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (a : R) (p : CPolynomial R) :
      (taylor a p).coeff 0 = eval a p

      The constant coefficient of the Taylor shift is evaluation at the shift point.