Documentation

Mathlib.Algebra.Polynomial.Derivative

The derivative map on polynomials #

Main definitions #

derivative p is the formal derivative of the polynomial p

Equations
theorem Polynomial.derivative_apply {R : Type u} [Semiring R] (p : Polynomial R) :
derivative p = p.sum fun (n : ) (a : R) => C (a * n) * X ^ (n - 1)
theorem Polynomial.coeff_derivative {R : Type u} [Semiring R] (p : Polynomial R) (n : ) :
(derivative p).coeff n = p.coeff (n + 1) * (n + 1)
@[simp]
theorem Polynomial.derivative_monomial {R : Type u} [Semiring R] (a : R) (n : ) :
derivative ((monomial n) a) = (monomial (n - 1)) (a * n)
@[simp]
theorem Polynomial.derivative_monomial_succ {R : Type u} [Semiring R] (a : R) (n : ) :
derivative ((monomial (n + 1)) a) = (monomial n) (a * (n + 1))
theorem Polynomial.derivative_C_mul_X {R : Type u} [Semiring R] (a : R) :
derivative (C a * X) = C a
theorem Polynomial.derivative_C_mul_X_pow {R : Type u} [Semiring R] (a : R) (n : ) :
derivative (C a * X ^ n) = C (a * n) * X ^ (n - 1)
theorem Polynomial.derivative_C_mul_X_sq {R : Type u} [Semiring R] (a : R) :
derivative (C a * X ^ 2) = C (a * 2) * X
theorem Polynomial.derivative_X_pow {R : Type u} [Semiring R] (n : ) :
derivative (X ^ n) = C n * X ^ (n - 1)
@[simp]
theorem Polynomial.derivative_X_pow_succ {R : Type u} [Semiring R] (n : ) :
derivative (X ^ (n + 1)) = C (n + 1) * X ^ n
@[simp]
theorem Polynomial.derivative_C {R : Type u} [Semiring R] {a : R} :
derivative (C a) = 0
@[simp]
@[simp]
@[simp]
theorem Polynomial.derivative_X_add_C {R : Type u} [Semiring R] (c : R) :
derivative (X + C c) = 1
theorem Polynomial.derivative_sum {R : Type u} {ι : Type y} [Semiring R] {s : Finset ι} {f : ιPolynomial R} :
derivative (∑ bs, f b) = bs, derivative (f b)
theorem Polynomial.iterate_derivative_sum {R : Type u} {ι : Type y} [Semiring R] (k : ) (s : Finset ι) (f : ιPolynomial R) :
(⇑derivative)^[k] (∑ bs, f b) = bs, (⇑derivative)^[k] (f b)
theorem Polynomial.derivative_smul {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] [IsScalarTower S R R] (s : S) (p : Polynomial R) :
@[simp]
theorem Polynomial.iterate_derivative_smul {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] [IsScalarTower S R R] (s : S) (p : Polynomial R) (k : ) :
(⇑derivative)^[k] (s p) = s (⇑derivative)^[k] p
@[simp]
theorem Polynomial.iterate_derivative_C_mul {R : Type u} [Semiring R] (a : R) (p : Polynomial R) (k : ) :
(⇑derivative)^[k] (C a * p) = C a * (⇑derivative)^[k] p
theorem Polynomial.derivative_C_mul {R : Type u} [Semiring R] (a : R) (p : Polynomial R) :
@[simp]
theorem Polynomial.derivative_natCast {R : Type u} [Semiring R] {n : } :
derivative n = 0
theorem Polynomial.iterate_derivative_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} {x : } (hx : p.natDegree < x) :
(⇑derivative)^[x] p = 0
@[simp]
theorem Polynomial.iterate_derivative_C {R : Type u} {a : R} [Semiring R] {k : } (h : 0 < k) :
(⇑derivative)^[k] (C a) = 0
@[simp]
theorem Polynomial.iterate_derivative_one {R : Type u} [Semiring R] {k : } (h : 0 < k) :
(⇑derivative)^[k] 1 = 0
@[simp]
theorem Polynomial.iterate_derivative_X {R : Type u} [Semiring R] {k : } (h : 1 < k) :
(⇑derivative)^[k] X = 0
@[simp]
theorem Polynomial.derivative_mul {R : Type u} [Semiring R] {f g : Polynomial R} :
theorem Polynomial.derivative_eval {R : Type u} [Semiring R] (p : Polynomial R) (x : R) :
eval x (derivative p) = p.sum fun (n : ) (a : R) => a * n * x ^ (n - 1)
@[simp]
theorem Polynomial.derivative_map {R : Type u} {S : Type v} [Semiring R] [Semiring S] (p : Polynomial R) (f : R →+* S) :
@[simp]
theorem Polynomial.iterate_derivative_map {R : Type u} {S : Type v} [Semiring R] [Semiring S] (p : Polynomial R) (f : R →+* S) (k : ) :
(⇑derivative)^[k] (map f p) = map f ((⇑derivative)^[k] p)
theorem Polynomial.derivative_natCast_mul {R : Type u} [Semiring R] {n : } {f : Polynomial R} :
derivative (n * f) = n * derivative f
@[simp]
theorem Polynomial.iterate_derivative_natCast_mul {R : Type u} [Semiring R] {n k : } {f : Polynomial R} :
(⇑derivative)^[k] (n * f) = n * (⇑derivative)^[k] f
theorem Polynomial.coeff_iterate_derivative {R : Type u} [Semiring R] {k : } (p : Polynomial R) (m : ) :
((⇑derivative)^[k] p).coeff m = (m + k).descFactorial k p.coeff (m + k)
theorem Polynomial.iterate_derivative_eq_sum {R : Type u} [Semiring R] (p : Polynomial R) (k : ) :
(⇑derivative)^[k] p = x((⇑derivative)^[k] p).support, C ((x + k).descFactorial k p.coeff (x + k)) * X ^ x
theorem Polynomial.iterate_derivative_eq_factorial_smul_sum {R : Type u} [Semiring R] (p : Polynomial R) (k : ) :
(⇑derivative)^[k] p = k.factorial x((⇑derivative)^[k] p).support, C ((x + k).choose k p.coeff (x + k)) * X ^ x
theorem Polynomial.iterate_derivative_mul {R : Type u} [Semiring R] {n : } (p q : Polynomial R) :
(⇑derivative)^[n] (p * q) = kFinset.range n.succ, n.choose k ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)

Iterated derivatives as a finite support function.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Polynomial.derivativeFinsupp_apply_toFun {R : Type u} [Semiring R] (p : Polynomial R) (x✝ : ) :
(derivativeFinsupp p) x✝ = (⇑derivative)^[x✝] p
theorem Polynomial.derivativeFinsupp_map {R : Type u} {S : Type v} [Semiring R] [Semiring S] (p : Polynomial R) (f : R →+* S) :
theorem Polynomial.derivative_pow_succ {R : Type u} [CommSemiring R] (p : Polynomial R) (n : ) :
derivative (p ^ (n + 1)) = C (n + 1) * p ^ n * derivative p
theorem Polynomial.derivative_pow {R : Type u} [CommSemiring R] (p : Polynomial R) (n : ) :
derivative (p ^ n) = C n * p ^ (n - 1) * derivative p
theorem Polynomial.pow_sub_one_dvd_derivative_of_pow_dvd {R : Type u} [CommSemiring R] {p q : Polynomial R} {n : } (dvd : q ^ n p) :
q ^ (n - 1) derivative p
theorem Polynomial.pow_sub_dvd_iterate_derivative_of_pow_dvd {R : Type u} [CommSemiring R] {p q : Polynomial R} {n : } (m : ) (dvd : q ^ n p) :
q ^ (n - m) (⇑derivative)^[m] p
theorem Polynomial.pow_sub_dvd_iterate_derivative_pow {R : Type u} [CommSemiring R] (p : Polynomial R) (n m : ) :
p ^ (n - m) (⇑derivative)^[m] (p ^ n)
theorem Polynomial.dvd_iterate_derivative_pow {R : Type u} [CommSemiring R] (f : Polynomial R) (n : ) {m : } (c : R) (hm : m 0) :
n eval c ((⇑derivative)^[m] (f ^ n))
theorem Polynomial.derivative_X_add_C_pow {R : Type u} [CommSemiring R] (c : R) (m : ) :
derivative ((X + C c) ^ m) = C m * (X + C c) ^ (m - 1)
theorem Polynomial.derivative_X_add_C_sq {R : Type u} [CommSemiring R] (c : R) :
derivative ((X + C c) ^ 2) = C 2 * (X + C c)
theorem Polynomial.iterate_derivative_X_add_pow {R : Type u} [CommSemiring R] (n k : ) (c : R) :
(⇑derivative)^[k] ((X + C c) ^ n) = n.descFactorial k (X + C c) ^ (n - k)

Chain rule for formal derivative of polynomials.

theorem Polynomial.derivative_prod {R : Type u} {ι : Type y} [CommSemiring R] [DecidableEq ι] {s : Multiset ι} {f : ιPolynomial R} :
derivative (Multiset.map f s).prod = (Multiset.map (fun (i : ι) => (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum
@[simp]
theorem Polynomial.iterate_derivative_neg {R : Type u} [Ring R] {f : Polynomial R} {k : } :
(⇑derivative)^[k] (-f) = -(⇑derivative)^[k] f
@[simp]
theorem Polynomial.derivative_X_sub_C {R : Type u} [Ring R] (c : R) :
derivative (X - C c) = 1
theorem Polynomial.iterate_derivative_sub {R : Type u} [Ring R] {k : } {f g : Polynomial R} :
(⇑derivative)^[k] (f - g) = (⇑derivative)^[k] f - (⇑derivative)^[k] g
@[simp]
theorem Polynomial.derivative_intCast {R : Type u} [Ring R] {n : } :
derivative n = 0
theorem Polynomial.derivative_intCast_mul {R : Type u} [Ring R] {n : } {f : Polynomial R} :
derivative (n * f) = n * derivative f
@[simp]
theorem Polynomial.iterate_derivative_intCast_mul {R : Type u} [Ring R] {n : } {k : } {f : Polynomial R} :
(⇑derivative)^[k] (n * f) = n * (⇑derivative)^[k] f
@[simp]
theorem Polynomial.iterate_derivative_comp_one_sub_X {R : Type u} [CommRing R] (p : Polynomial R) (k : ) :
(⇑derivative)^[k] (p.comp (1 - X)) = (-1) ^ k * ((⇑derivative)^[k] p).comp (1 - X)
theorem Polynomial.eval_multiset_prod_X_sub_C_derivative {R : Type u} [CommRing R] [DecidableEq R] {S : Multiset R} {r : R} (hr : r S) :
eval r (derivative (Multiset.map (fun (a : R) => X - C a) S).prod) = (Multiset.map (fun (a : R) => r - a) (S.erase r)).prod
theorem Polynomial.derivative_X_sub_C_pow {R : Type u} [CommRing R] (c : R) (m : ) :
derivative ((X - C c) ^ m) = C m * (X - C c) ^ (m - 1)
theorem Polynomial.derivative_X_sub_C_sq {R : Type u} [CommRing R] (c : R) :
derivative ((X - C c) ^ 2) = C 2 * (X - C c)
theorem Polynomial.iterate_derivative_X_sub_pow {R : Type u} [CommRing R] (n k : ) (c : R) :
(⇑derivative)^[k] ((X - C c) ^ n) = n.descFactorial k (X - C c) ^ (n - k)
theorem Polynomial.iterate_derivative_X_sub_pow_self {R : Type u} [CommRing R] (n : ) (c : R) :
(⇑derivative)^[n] ((X - C c) ^ n) = n.factorial
theorem Polynomial.derivative_pow_eq_zero {R : Type u} [CommSemiring R] [NoZeroDivisors R] {n : } (chn : n 0) {a : Polynomial R} :