Theory of iterated derivative #
We define and prove some lemmas about iterated (formal) derivative for polynomials over a semiring.
iterated_deriv f n
is the n
-th formal derivative of the polynomial f
Equations
Informal translation
The $0$th derivative of a polynomial is the polynomial itself.
Informal translation
Let $R$ be a semiring and let $f$ be a polynomial over $R$. Then the $(n+1)$-th derivative of $f$ is the derivative of the $n$-th derivative of $f$.
Informal translation
The $n$-th derivative of the zero polynomial is the zero polynomial.
Informal translation
Let $p, q$ be polynomials over a semiring $R$. Then the $n$-th derivative of $p+q$ is the sum of the $n$-th derivatives of $p$ and $q$.
Informal translation
Let $R$ be a semiring, $S$ a monoid, and $p$ a polynomial over $R$. Then the $n$-th derivative of $s\cdot p$ is $s\cdot p^{(n)}$.
Informal translation
The $0$th derivative of $X$ is $X$.
Informal translation
The first derivative of $x$ is $1$.
Informal translation
The $n$-th derivative of $x$ is $0$ for $n>1$.
Informal translation
The $0$th derivative of the constant polynomial $r$ is the constant polynomial $r$.
Informal translation
The $n$-th derivative of the constant function $f(x)=r$ is zero.
Informal translation
The $0$th derivative of $1$ is $1$.
Informal translation
The $n$-th derivative of $1$ is $0$ for $n>0$.
Informal translation
Let $f$ be a polynomial over a semiring $R$. Then the coefficient of $x^m$ in the $k$-th derivative of $f$ is equal to the product of the numbers $1,2,\ldots,m$ times the coefficient of $x^{m+k}$ in $f$.
Informal translation
Let $f$ be a polynomial over a semiring $R$. Then the coefficient of $x^m$ in the $k$-th derivative of $f$ is equal to $(m+k)!$ times the coefficient of $x^{m+k}$ in $f$.
Informal translation
Let $f$ be a polynomial over a semiring $R$. If the degree of $f$ is less than $n$, then the $n$-th derivative of $f$ is zero.
Informal translation
Let $R$ be a semiring and let $p, q$ be polynomials over $R$. Then the $n$-th derivative of $pq$ is equal to the sum of the $n$-th derivatives of $p$ and $q$.
Informal translation
The $n$-th derivative of $-p$ is $-p^{(n)}$.
Informal translation
Let $p, q$ be polynomials over a ring $R$. Then the $n$th derivative of $p-q$ is the $n$th derivative of $p$ minus the $n$th derivative of $q$.