# 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
theorem polynomial.iterated_deriv_succ {R : Type u} [semiring R] (f : polynomial R) (n : ) :
f.iterated_deriv (n + 1) =
@[simp]
theorem polynomial.iterated_deriv_zero_left {R : Type u} [semiring R] (n : ) :
= 0
@[simp]
theorem polynomial.iterated_deriv_add {R : Type u} [semiring R] (p q : polynomial R) (n : ) :
(p + q).iterated_deriv n = +
@[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
@[simp]
theorem polynomial.iterated_deriv_X_zero {R : Type u} [semiring R] :
@[simp]
theorem polynomial.iterated_deriv_X_one {R : Type u} [semiring R] :
@[simp]
theorem polynomial.iterated_deriv_X {R : Type u} [semiring R] (n : ) (h : 1 < n) :
@[simp]
theorem polynomial.iterated_deriv_C_zero {R : Type u} [semiring R] (r : R) :
@[simp]
theorem polynomial.iterated_deriv_C {R : Type u} [semiring R] (r : R) (n : ) (h : 0 < n) :
= 0
@[simp]
theorem polynomial.iterated_deriv_one_zero {R : Type u} [semiring R] :
= 1
@[simp]
theorem polynomial.iterated_deriv_one {R : Type u} [semiring R] (n : ) :
0 < n = 0
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)
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)
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
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))
@[simp]
theorem polynomial.iterated_deriv_neg {R : Type u} [ring R] (p : polynomial R) (n : ) :
@[simp]
theorem polynomial.iterated_deriv_sub {R : Type u} [ring R] (p q : polynomial R) (n : ) :
(p - q).iterated_deriv n = -