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
@[simp]
theorem
polynomial.iterated_deriv_zero_right
{R : Type u}
[semiring R]
(f : polynomial R) :
f.iterated_deriv 0 = f
theorem
polynomial.iterated_deriv_succ
{R : Type u}
[semiring R]
(f : polynomial R)
(n : ℕ) :
f.iterated_deriv (n + 1) = (f.iterated_deriv n).derivative
@[simp]
theorem
polynomial.iterated_deriv_zero_left
{R : Type u}
[semiring R]
(n : ℕ) :
0.iterated_deriv n = 0
@[simp]
theorem
polynomial.iterated_deriv_add
{R : Type u}
[semiring R]
(p q : polynomial R)
(n : ℕ) :
(p + q).iterated_deriv n = p.iterated_deriv n + q.iterated_deriv n
@[simp]
theorem
polynomial.iterated_deriv_smul
{R : Type u}
[semiring R]
(r : R)
(p : polynomial R)
(n : ℕ) :
(r • p).iterated_deriv n = r • p.iterated_deriv n
@[simp]
@[simp]
@[simp]
@[simp]
theorem
polynomial.iterated_deriv_C_zero
{R : Type u}
[semiring R]
(r : R) :
(⇑polynomial.C r).iterated_deriv 0 = ⇑polynomial.C r
@[simp]
theorem
polynomial.iterated_deriv_C
{R : Type u}
[semiring R]
(r : R)
(n : ℕ)
(h : 0 < n) :
(⇑polynomial.C r).iterated_deriv n = 0
@[simp]
@[simp]
theorem
polynomial.iterated_deriv_one
{R : Type u}
[semiring R]
(n : ℕ) :
0 < n → 1.iterated_deriv n = 0
@[simp]
theorem
polynomial.iterated_deriv_neg
{R : Type u}
[ring R]
(p : polynomial R)
(n : ℕ) :
(-p).iterated_deriv n = -p.iterated_deriv n
@[simp]
theorem
polynomial.iterated_deriv_sub
{R : Type u}
[ring R]
(p q : polynomial R)
(n : ℕ) :
(p - q).iterated_deriv n = p.iterated_deriv n - q.iterated_deriv n
theorem
polynomial.coeff_iterated_deriv_as_prod_Ico
{R : Type u}
[comm_semiring R]
(f : polynomial R)
(k m : ℕ) :
theorem
polynomial.coeff_iterated_deriv_as_prod_range
{R : Type u}
[comm_semiring R]
(f : polynomial R)
(k m : ℕ) :
theorem
polynomial.iterated_deriv_eq_zero_of_nat_degree_lt
{R : Type u}
[comm_semiring R]
(f : polynomial R)
(n : ℕ)
(h : f.nat_degree < n) :
f.iterated_deriv n = 0
theorem
polynomial.iterated_deriv_mul
{R : Type u}
[comm_semiring R]
(p q : polynomial R)
(n : ℕ) :
(p * q).iterated_deriv n = ∑ (k : ℕ) in finset.range n.succ, ((⇑polynomial.C ↑(n.choose k)) * p.iterated_deriv (n - k)) * q.iterated_deriv k