mathlibdocumentation

data.polynomial.iterated_deriv

Theory of iterated derivative #

We define and prove some lemmas about iterated (formal) derivative for polynomials over a semiring.

noncomputable def polynomial.iterated_deriv {R : Type u} [semiring R] (f : polynomial R) (n : ) :

iterated_deriv f n is the n-th formal derivative of the polynomial f

Equations
@[simp]
theorem polynomial.iterated_deriv_zero_right {R : Type u} [semiring R] (f : polynomial R) :
= f
Informal translation

The $0$th derivative of a polynomial is the polynomial itself.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem polynomial.iterated_deriv_succ {R : Type u} [semiring R] (f : polynomial R) (n : ) :
f.iterated_deriv (n + 1) =
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$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem polynomial.iterated_deriv_zero_left {R : Type u} [semiring R] (n : ) :
= 0
Informal translation

The $n$-th derivative of the zero polynomial is the zero polynomial.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem polynomial.iterated_deriv_add {R : Type u} [semiring R] (p q : polynomial R) (n : ) :
(p + q).iterated_deriv n = +
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$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem polynomial.iterated_deriv_smul {R : Type u} [semiring R] (p : polynomial R) (n : ) {S : Type u_1} [monoid S] [ R] [ R] (s : S) :
(s p).iterated_deriv n = s
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)}$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem polynomial.iterated_deriv_X_zero {R : Type u} [semiring R] :
Informal translation

The $0$th derivative of $X$ is $X$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem polynomial.iterated_deriv_X_one {R : Type u} [semiring R] :
Informal translation

The first derivative of $x$ is $1$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem polynomial.iterated_deriv_X {R : Type u} [semiring R] (n : ) (h : 1 < n) :
Informal translation

The $n$-th derivative of $x$ is $0$ for $n>1$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem polynomial.iterated_deriv_C_zero {R : Type u} [semiring R] (r : R) :
Informal translation

The $0$th derivative of the constant polynomial $r$ is the constant polynomial $r$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem polynomial.iterated_deriv_C {R : Type u} [semiring R] (r : R) (n : ) (h : 0 < n) :
= 0
Informal translation

The $n$-th derivative of the constant function $f(x)=r$ is zero.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem polynomial.iterated_deriv_one_zero {R : Type u} [semiring R] :
= 1
Informal translation

The $0$th derivative of $1$ is $1$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem polynomial.iterated_deriv_one {R : Type u} [semiring R] (n : ) :
0 < n = 0
Informal translation

The $n$-th derivative of $1$ is $0$ for $n>0$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem polynomial.coeff_iterated_deriv_as_prod_Ico {R : Type u} [semiring R] (f : polynomial R) (k m : ) :
(f.iterated_deriv k).coeff m = (m + k.succ)).prod (λ (i : ), i) f.coeff (m + k)
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$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem polynomial.coeff_iterated_deriv_as_prod_range {R : Type u} [semiring R] (f : polynomial R) (k m : ) :
(f.iterated_deriv k).coeff m = (finset.range k).prod (λ (i : ), m + k - i) f.coeff (m + k)
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$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem polynomial.iterated_deriv_eq_zero_of_nat_degree_lt {R : Type u} [semiring R] (f : polynomial R) (n : ) (h : f.nat_degree < n) :
= 0
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.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem polynomial.iterated_deriv_mul {R : Type u} [semiring R] (p q : polynomial R) (n : ) :
(p * q).iterated_deriv n = (finset.range n.succ).sum (λ (k : ), n.choose k (p.iterated_deriv (n - k) * q.iterated_deriv k))
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$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem polynomial.iterated_deriv_neg {R : Type u} [ring R] (p : polynomial R) (n : ) :
Informal translation

The $n$-th derivative of $-p$ is $-p^{(n)}$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem polynomial.iterated_deriv_sub {R : Type u} [ring R] (p q : polynomial R) (n : ) :
(p - q).iterated_deriv 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$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?