Documentation

Mathlib.Algebra.Polynomial.Derivative

The derivative map on polynomials #

Main definitions #

derivative p is the formal derivative of the polynomial p

Equations
  • Polynomial.derivative = { toFun := fun (p : Polynomial R) => p.sum fun (n : ) (a : R) => Polynomial.C (a * n) * Polynomial.X ^ (n - 1), map_add' := , map_smul' := }
Instances For
    theorem Polynomial.derivative_apply {R : Type u} [Semiring R] (p : Polynomial R) :
    Polynomial.derivative p = p.sum fun (n : ) (a : R) => Polynomial.C (a * n) * Polynomial.X ^ (n - 1)
    theorem Polynomial.coeff_derivative {R : Type u} [Semiring R] (p : Polynomial R) (n : ) :
    (Polynomial.derivative p).coeff n = p.coeff (n + 1) * (n + 1)
    theorem Polynomial.derivative_zero {R : Type u} [Semiring R] :
    Polynomial.derivative 0 = 0
    theorem Polynomial.iterate_derivative_zero {R : Type u} [Semiring R] {k : } :
    (Polynomial.derivative)^[k] 0 = 0
    @[simp]
    theorem Polynomial.derivative_monomial {R : Type u} [Semiring R] (a : R) (n : ) :
    Polynomial.derivative ((Polynomial.monomial n) a) = (Polynomial.monomial (n - 1)) (a * n)
    theorem Polynomial.derivative_C_mul_X {R : Type u} [Semiring R] (a : R) :
    Polynomial.derivative (Polynomial.C a * Polynomial.X) = Polynomial.C a
    theorem Polynomial.derivative_C_mul_X_pow {R : Type u} [Semiring R] (a : R) (n : ) :
    Polynomial.derivative (Polynomial.C a * Polynomial.X ^ n) = Polynomial.C (a * n) * Polynomial.X ^ (n - 1)
    theorem Polynomial.derivative_C_mul_X_sq {R : Type u} [Semiring R] (a : R) :
    Polynomial.derivative (Polynomial.C a * Polynomial.X ^ 2) = Polynomial.C (a * 2) * Polynomial.X
    @[simp]
    theorem Polynomial.derivative_X_pow {R : Type u} [Semiring R] (n : ) :
    Polynomial.derivative (Polynomial.X ^ n) = Polynomial.C n * Polynomial.X ^ (n - 1)
    theorem Polynomial.derivative_X_sq {R : Type u} [Semiring R] :
    Polynomial.derivative (Polynomial.X ^ 2) = Polynomial.C 2 * Polynomial.X
    @[simp]
    theorem Polynomial.derivative_C {R : Type u} [Semiring R] {a : R} :
    Polynomial.derivative (Polynomial.C a) = 0
    theorem Polynomial.derivative_of_natDegree_zero {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.natDegree = 0) :
    Polynomial.derivative p = 0
    @[simp]
    theorem Polynomial.derivative_X {R : Type u} [Semiring R] :
    Polynomial.derivative Polynomial.X = 1
    @[simp]
    theorem Polynomial.derivative_one {R : Type u} [Semiring R] :
    Polynomial.derivative 1 = 0
    theorem Polynomial.derivative_add {R : Type u} [Semiring R] {f : Polynomial R} {g : Polynomial R} :
    Polynomial.derivative (f + g) = Polynomial.derivative f + Polynomial.derivative g
    theorem Polynomial.derivative_X_add_C {R : Type u} [Semiring R] (c : R) :
    Polynomial.derivative (Polynomial.X + Polynomial.C c) = 1
    theorem Polynomial.derivative_sum {R : Type u} {ι : Type y} [Semiring R] {s : Finset ι} {f : ιPolynomial R} :
    Polynomial.derivative (bs, f b) = bs, Polynomial.derivative (f b)
    theorem Polynomial.derivative_smul {R : Type u} [Semiring R] {S : Type u_1} [Monoid S] [DistribMulAction S R] [IsScalarTower S R R] (s : S) (p : Polynomial R) :
    Polynomial.derivative (s p) = s Polynomial.derivative p
    @[simp]
    theorem Polynomial.iterate_derivative_smul {R : Type u} [Semiring R] {S : Type u_1} [Monoid S] [DistribMulAction S R] [IsScalarTower S R R] (s : S) (p : Polynomial R) (k : ) :
    (Polynomial.derivative)^[k] (s p) = s (Polynomial.derivative)^[k] p
    @[simp]
    theorem Polynomial.iterate_derivative_C_mul {R : Type u} [Semiring R] (a : R) (p : Polynomial R) (k : ) :
    (Polynomial.derivative)^[k] (Polynomial.C a * p) = Polynomial.C a * (Polynomial.derivative)^[k] p
    theorem Polynomial.of_mem_support_derivative {R : Type u} [Semiring R] {p : Polynomial R} {n : } (h : n (Polynomial.derivative p).support) :
    n + 1 p.support
    theorem Polynomial.degree_derivative_lt {R : Type u} [Semiring R] {p : Polynomial R} (hp : p 0) :
    (Polynomial.derivative p).degree < p.degree
    theorem Polynomial.degree_derivative_le {R : Type u} [Semiring R] {p : Polynomial R} :
    (Polynomial.derivative p).degree p.degree
    theorem Polynomial.natDegree_derivative_lt {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.natDegree 0) :
    (Polynomial.derivative p).natDegree < p.natDegree
    theorem Polynomial.natDegree_derivative_le {R : Type u} [Semiring R] (p : Polynomial R) :
    (Polynomial.derivative p).natDegree p.natDegree - 1
    theorem Polynomial.natDegree_iterate_derivative {R : Type u} [Semiring R] (p : Polynomial R) (k : ) :
    ((Polynomial.derivative)^[k] p).natDegree p.natDegree - k
    @[simp]
    theorem Polynomial.derivative_natCast {R : Type u} [Semiring R] {n : } :
    Polynomial.derivative n = 0
    @[deprecated Polynomial.derivative_natCast]
    theorem Polynomial.derivative_nat_cast {R : Type u} [Semiring R] {n : } :
    Polynomial.derivative n = 0

    Alias of Polynomial.derivative_natCast.

    @[simp]
    theorem Polynomial.derivative_ofNat {R : Type u} [Semiring R] (n : ) [n.AtLeastTwo] :
    Polynomial.derivative (OfNat.ofNat n) = 0
    theorem Polynomial.iterate_derivative_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} {x : } (hx : p.natDegree < x) :
    (Polynomial.derivative)^[x] p = 0
    @[simp]
    theorem Polynomial.iterate_derivative_C {R : Type u} {a : R} [Semiring R] {k : } (h : 0 < k) :
    (Polynomial.derivative)^[k] (Polynomial.C a) = 0
    @[simp]
    theorem Polynomial.iterate_derivative_one {R : Type u} [Semiring R] {k : } (h : 0 < k) :
    (Polynomial.derivative)^[k] 1 = 0
    @[simp]
    theorem Polynomial.iterate_derivative_X {R : Type u} [Semiring R] {k : } (h : 1 < k) :
    (Polynomial.derivative)^[k] Polynomial.X = 0
    theorem Polynomial.natDegree_eq_zero_of_derivative_eq_zero {R : Type u} [Semiring R] [NoZeroSMulDivisors R] {f : Polynomial R} (h : Polynomial.derivative f = 0) :
    f.natDegree = 0
    theorem Polynomial.eq_C_of_derivative_eq_zero {R : Type u} [Semiring R] [NoZeroSMulDivisors R] {f : Polynomial R} (h : Polynomial.derivative f = 0) :
    f = Polynomial.C (f.coeff 0)
    @[simp]
    theorem Polynomial.derivative_mul {R : Type u} [Semiring R] {f : Polynomial R} {g : Polynomial R} :
    Polynomial.derivative (f * g) = Polynomial.derivative f * g + f * Polynomial.derivative g
    theorem Polynomial.derivative_eval {R : Type u} [Semiring R] (p : Polynomial R) (x : R) :
    Polynomial.eval x (Polynomial.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) :
    Polynomial.derivative (Polynomial.map f p) = Polynomial.map f (Polynomial.derivative p)
    @[simp]
    theorem Polynomial.iterate_derivative_map {R : Type u} {S : Type v} [Semiring R] [Semiring S] (p : Polynomial R) (f : R →+* S) (k : ) :
    (Polynomial.derivative)^[k] (Polynomial.map f p) = Polynomial.map f ((Polynomial.derivative)^[k] p)
    theorem Polynomial.derivative_natCast_mul {R : Type u} [Semiring R] {n : } {f : Polynomial R} :
    Polynomial.derivative (n * f) = n * Polynomial.derivative f
    @[deprecated Polynomial.derivative_natCast_mul]
    theorem Polynomial.derivative_nat_cast_mul {R : Type u} [Semiring R] {n : } {f : Polynomial R} :
    Polynomial.derivative (n * f) = n * Polynomial.derivative f

    Alias of Polynomial.derivative_natCast_mul.

    @[simp]
    theorem Polynomial.iterate_derivative_natCast_mul {R : Type u} [Semiring R] {n : } {k : } {f : Polynomial R} :
    (Polynomial.derivative)^[k] (n * f) = n * (Polynomial.derivative)^[k] f
    @[deprecated Polynomial.iterate_derivative_natCast_mul]
    theorem Polynomial.iterate_derivative_nat_cast_mul {R : Type u} [Semiring R] {n : } {k : } {f : Polynomial R} :
    (Polynomial.derivative)^[k] (n * f) = n * (Polynomial.derivative)^[k] f

    Alias of Polynomial.iterate_derivative_natCast_mul.

    theorem Polynomial.mem_support_derivative {R : Type u} [Semiring R] [NoZeroSMulDivisors R] (p : Polynomial R) (n : ) :
    n (Polynomial.derivative p).support n + 1 p.support
    @[simp]
    theorem Polynomial.degree_derivative_eq {R : Type u} [Semiring R] [NoZeroSMulDivisors R] (p : Polynomial R) (hp : 0 < p.natDegree) :
    (Polynomial.derivative p).degree = (p.natDegree - 1)
    theorem Polynomial.coeff_iterate_derivative {R : Type u} [Semiring R] {k : } (p : Polynomial R) (m : ) :
    ((Polynomial.derivative)^[k] p).coeff m = (m + k).descFactorial k p.coeff (m + k)
    theorem Polynomial.iterate_derivative_mul {R : Type u} [Semiring R] {n : } (p : Polynomial R) (q : Polynomial R) :
    (Polynomial.derivative)^[n] (p * q) = kFinset.range n.succ, n.choose k ((Polynomial.derivative)^[n - k] p * (Polynomial.derivative)^[k] q)
    theorem Polynomial.derivative_pow_succ {R : Type u} [CommSemiring R] (p : Polynomial R) (n : ) :
    Polynomial.derivative (p ^ (n + 1)) = Polynomial.C (n + 1) * p ^ n * Polynomial.derivative p
    theorem Polynomial.derivative_pow {R : Type u} [CommSemiring R] (p : Polynomial R) (n : ) :
    Polynomial.derivative (p ^ n) = Polynomial.C n * p ^ (n - 1) * Polynomial.derivative p
    theorem Polynomial.derivative_sq {R : Type u} [CommSemiring R] (p : Polynomial R) :
    Polynomial.derivative (p ^ 2) = Polynomial.C 2 * p * Polynomial.derivative p
    theorem Polynomial.pow_sub_one_dvd_derivative_of_pow_dvd {R : Type u} [CommSemiring R] {p : Polynomial R} {q : Polynomial R} {n : } (dvd : q ^ n p) :
    q ^ (n - 1) Polynomial.derivative p
    theorem Polynomial.pow_sub_dvd_iterate_derivative_of_pow_dvd {R : Type u} [CommSemiring R] {p : Polynomial R} {q : Polynomial R} {n : } (m : ) (dvd : q ^ n p) :
    q ^ (n - m) (Polynomial.derivative)^[m] p
    theorem Polynomial.pow_sub_dvd_iterate_derivative_pow {R : Type u} [CommSemiring R] (p : Polynomial R) (n : ) (m : ) :
    p ^ (n - m) (Polynomial.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 Polynomial.eval c ((Polynomial.derivative)^[m] (f ^ n))
    theorem Polynomial.iterate_derivative_X_pow_eq_natCast_mul {R : Type u} [CommSemiring R] (n : ) (k : ) :
    (Polynomial.derivative)^[k] (Polynomial.X ^ n) = (n.descFactorial k) * Polynomial.X ^ (n - k)
    @[deprecated Polynomial.iterate_derivative_X_pow_eq_natCast_mul]
    theorem Polynomial.iterate_derivative_X_pow_eq_nat_cast_mul {R : Type u} [CommSemiring R] (n : ) (k : ) :
    (Polynomial.derivative)^[k] (Polynomial.X ^ n) = (n.descFactorial k) * Polynomial.X ^ (n - k)

    Alias of Polynomial.iterate_derivative_X_pow_eq_natCast_mul.

    theorem Polynomial.iterate_derivative_X_pow_eq_C_mul {R : Type u} [CommSemiring R] (n : ) (k : ) :
    (Polynomial.derivative)^[k] (Polynomial.X ^ n) = Polynomial.C (n.descFactorial k) * Polynomial.X ^ (n - k)
    theorem Polynomial.iterate_derivative_X_pow_eq_smul {R : Type u} [CommSemiring R] (n : ) (k : ) :
    (Polynomial.derivative)^[k] (Polynomial.X ^ n) = (n.descFactorial k) Polynomial.X ^ (n - k)
    theorem Polynomial.derivative_X_add_C_pow {R : Type u} [CommSemiring R] (c : R) (m : ) :
    Polynomial.derivative ((Polynomial.X + Polynomial.C c) ^ m) = Polynomial.C m * (Polynomial.X + Polynomial.C c) ^ (m - 1)
    theorem Polynomial.derivative_X_add_C_sq {R : Type u} [CommSemiring R] (c : R) :
    Polynomial.derivative ((Polynomial.X + Polynomial.C c) ^ 2) = Polynomial.C 2 * (Polynomial.X + Polynomial.C c)
    theorem Polynomial.iterate_derivative_X_add_pow {R : Type u} [CommSemiring R] (n : ) (k : ) (c : R) :
    (Polynomial.derivative)^[k] ((Polynomial.X + Polynomial.C c) ^ n) = n.descFactorial k (Polynomial.X + Polynomial.C c) ^ (n - k)
    theorem Polynomial.derivative_comp {R : Type u} [CommSemiring R] (p : Polynomial R) (q : Polynomial R) :
    Polynomial.derivative (p.comp q) = Polynomial.derivative q * (Polynomial.derivative p).comp q
    theorem Polynomial.derivative_eval₂_C {R : Type u} [CommSemiring R] (p : Polynomial R) (q : Polynomial R) :
    Polynomial.derivative (Polynomial.eval₂ Polynomial.C q p) = Polynomial.eval₂ Polynomial.C q (Polynomial.derivative p) * Polynomial.derivative q

    Chain rule for formal derivative of polynomials.

    theorem Polynomial.derivative_prod {R : Type u} {ι : Type y} [CommSemiring R] [DecidableEq ι] {s : Multiset ι} {f : ιPolynomial R} :
    Polynomial.derivative (Multiset.map f s).prod = (Multiset.map (fun (i : ι) => (Multiset.map f (s.erase i)).prod * Polynomial.derivative (f i)) s).sum
    theorem Polynomial.derivative_neg {R : Type u} [Ring R] (f : Polynomial R) :
    Polynomial.derivative (-f) = -Polynomial.derivative f
    theorem Polynomial.iterate_derivative_neg {R : Type u} [Ring R] {f : Polynomial R} {k : } :
    (Polynomial.derivative)^[k] (-f) = -(Polynomial.derivative)^[k] f
    theorem Polynomial.derivative_sub {R : Type u} [Ring R] {f : Polynomial R} {g : Polynomial R} :
    Polynomial.derivative (f - g) = Polynomial.derivative f - Polynomial.derivative g
    theorem Polynomial.derivative_X_sub_C {R : Type u} [Ring R] (c : R) :
    Polynomial.derivative (Polynomial.X - Polynomial.C c) = 1
    theorem Polynomial.iterate_derivative_sub {R : Type u} [Ring R] {k : } {f : Polynomial R} {g : Polynomial R} :
    (Polynomial.derivative)^[k] (f - g) = (Polynomial.derivative)^[k] f - (Polynomial.derivative)^[k] g
    @[simp]
    theorem Polynomial.derivative_intCast {R : Type u} [Ring R] {n : } :
    Polynomial.derivative n = 0
    @[deprecated Polynomial.derivative_intCast]
    theorem Polynomial.derivative_int_cast {R : Type u} [Ring R] {n : } :
    Polynomial.derivative n = 0

    Alias of Polynomial.derivative_intCast.

    theorem Polynomial.derivative_intCast_mul {R : Type u} [Ring R] {n : } {f : Polynomial R} :
    Polynomial.derivative (n * f) = n * Polynomial.derivative f
    @[deprecated Polynomial.derivative_intCast_mul]
    theorem Polynomial.derivative_int_cast_mul {R : Type u} [Ring R] {n : } {f : Polynomial R} :
    Polynomial.derivative (n * f) = n * Polynomial.derivative f

    Alias of Polynomial.derivative_intCast_mul.

    @[simp]
    theorem Polynomial.iterate_derivative_intCast_mul {R : Type u} [Ring R] {n : } {k : } {f : Polynomial R} :
    (Polynomial.derivative)^[k] (n * f) = n * (Polynomial.derivative)^[k] f
    @[deprecated Polynomial.iterate_derivative_intCast_mul]
    theorem Polynomial.iterate_derivative_int_cast_mul {R : Type u} [Ring R] {n : } {k : } {f : Polynomial R} :
    (Polynomial.derivative)^[k] (n * f) = n * (Polynomial.derivative)^[k] f

    Alias of Polynomial.iterate_derivative_intCast_mul.

    theorem Polynomial.derivative_comp_one_sub_X {R : Type u} [CommRing R] (p : Polynomial R) :
    Polynomial.derivative (p.comp (1 - Polynomial.X)) = -(Polynomial.derivative p).comp (1 - Polynomial.X)
    @[simp]
    theorem Polynomial.iterate_derivative_comp_one_sub_X {R : Type u} [CommRing R] (p : Polynomial R) (k : ) :
    (Polynomial.derivative)^[k] (p.comp (1 - Polynomial.X)) = (-1) ^ k * ((Polynomial.derivative)^[k] p).comp (1 - Polynomial.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) :
    Polynomial.eval r (Polynomial.derivative (Multiset.map (fun (a : R) => Polynomial.X - Polynomial.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 : ) :
    Polynomial.derivative ((Polynomial.X - Polynomial.C c) ^ m) = Polynomial.C m * (Polynomial.X - Polynomial.C c) ^ (m - 1)
    theorem Polynomial.derivative_X_sub_C_sq {R : Type u} [CommRing R] (c : R) :
    Polynomial.derivative ((Polynomial.X - Polynomial.C c) ^ 2) = Polynomial.C 2 * (Polynomial.X - Polynomial.C c)
    theorem Polynomial.iterate_derivative_X_sub_pow {R : Type u} [CommRing R] (n : ) (k : ) (c : R) :
    (Polynomial.derivative)^[k] ((Polynomial.X - Polynomial.C c) ^ n) = n.descFactorial k (Polynomial.X - Polynomial.C c) ^ (n - k)
    theorem Polynomial.iterate_derivative_X_sub_pow_self {R : Type u} [CommRing R] (n : ) (c : R) :
    (Polynomial.derivative)^[n] ((Polynomial.X - Polynomial.C c) ^ n) = n.factorial