mathlib documentation

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) :
@[simp]
theorem polynomial.iterated_deriv_zero_left {R : Type u} [semiring R] (n : ) :
@[simp]
theorem polynomial.iterated_deriv_add {R : Type u} [semiring R] (p q : polynomial R) (n : ) :
@[simp]
theorem polynomial.iterated_deriv_smul {R : Type u} [semiring R] (p : polynomial R) (n : ) {S : Type u_1} [monoid S] [distrib_mul_action S R] [is_scalar_tower S R R] (s : S) :
@[simp]
theorem polynomial.iterated_deriv_X {R : Type u} [semiring R] (n : ) (h : 1 < n) :
@[simp]
theorem polynomial.iterated_deriv_C {R : Type u} [semiring R] (r : R) (n : ) (h : 0 < n) :
@[simp]
theorem polynomial.iterated_deriv_one_zero {R : Type u} [semiring R] :
@[simp]
theorem polynomial.iterated_deriv_one {R : Type u} [semiring R] (n : ) :
0 < n1.iterated_deriv 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 = (finset.Ico m.succ (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_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 : ) :