The derivative map on polynomials

Main definitions

• Polynomial.derivative: The formal derivative of polynomials, expressed as a linear map.

def Polynomial.derivative {R : Type u} [Semiring R] : Polynomial R →ₗ[R] Polynomial R

derivative p is the formal derivative of the polynomial p

Equations

• One or more equations did not get rendered due to their size.

theorem Polynomial.derivative_apply {R : Type u} [Semiring R] (p : Polynomial R) : Polynomial.derivative p = Polynomial.sum p 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.coeff (Polynomial.derivative p) n = Polynomial.coeff p (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 : Polynomial.natDegree p = 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_bit0 {R : Type u} [Semiring R] {a : Polynomial R} : Polynomial.derivative (bit0 a) = bit0 (Polynomial.derivative a)

theorem Polynomial.derivative_bit1 {R : Type u} [Semiring R] {a : Polynomial R} : Polynomial.derivative (bit1 a) = bit0 (Polynomial.derivative a)

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 (Finset.sum s fun (b : ι) => f b) = Finset.sum s fun (b : ι) => 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.support (Polynomial.derivative p)) : n + 1 ∈ Polynomial.support p

theorem Polynomial.degree_derivative_lt {R : Type u} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) : Polynomial.degree (Polynomial.derivative p) < Polynomial.degree p

theorem Polynomial.degree_derivative_le {R : Type u} [Semiring R] {p : Polynomial R} : Polynomial.degree (Polynomial.derivative p) ≤ Polynomial.degree p

theorem Polynomial.natDegree_derivative_lt {R : Type u} [Semiring R] {p : Polynomial R} (hp : Polynomial.natDegree p ≠ 0) : Polynomial.natDegree (Polynomial.derivative p) < Polynomial.natDegree p

theorem Polynomial.natDegree_derivative_le {R : Type u} [Semiring R] (p : Polynomial R) : Polynomial.natDegree (Polynomial.derivative p) ≤ Polynomial.natDegree p - 1

theorem Polynomial.natDegree_iterate_derivative {R : Type u} [Semiring R] (p : Polynomial R) (k : ℕ) : Polynomial.natDegree ((⇑Polynomial.derivative)^[k] p) ≤ Polynomial.natDegree p - k

@[simp]

theorem Polynomial.derivative_natCast {R : Type u} [Semiring R] {n : ℕ} : Polynomial.derivative ↑n = 0

@[simp]

theorem Polynomial.derivative_ofNat {R : Type u} [Semiring R] (n : ℕ) [Nat.AtLeastTwo n] : Polynomial.derivative (OfNat.ofNat n) = 0

theorem Polynomial.iterate_derivative_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} {x : ℕ} (hx : Polynomial.natDegree p < 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) : Polynomial.natDegree f = 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 (Polynomial.coeff f 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) = Polynomial.sum p 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

@[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

theorem Polynomial.mem_support_derivative {R : Type u} [Semiring R] [NoZeroSMulDivisors ℕ R] (p : Polynomial R) (n : ℕ) : n ∈ Polynomial.support (Polynomial.derivative p) ↔ n + 1 ∈ Polynomial.support p

@[simp]

theorem Polynomial.degree_derivative_eq {R : Type u} [Semiring R] [NoZeroSMulDivisors ℕ R] (p : Polynomial R) (hp : 0 < Polynomial.natDegree p) : Polynomial.degree (Polynomial.derivative p) = ↑(Polynomial.natDegree p - 1)

theorem Polynomial.coeff_iterate_derivative {R : Type u} [Semiring R] {k : ℕ} (p : Polynomial R) (m : ℕ) : Polynomial.coeff ((⇑Polynomial.derivative)^[k] p) m = Nat.descFactorial (m + k) k • Polynomial.coeff p (m + k)

theorem Polynomial.iterate_derivative_mul {R : Type u} [Semiring R] {n : ℕ} (p : Polynomial R) (q : Polynomial R) : (⇑Polynomial.derivative)^[n] (p * q) = Finset.sum (Finset.range (Nat.succ n)) fun (k : ℕ) => Nat.choose n 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) = ↑(Nat.descFactorial n k) * Polynomial.X ^ (n - k)

theorem Polynomial.iterate_derivative_X_pow_eq_C_mul {R : Type u} [CommSemiring R] (n : ℕ) (k : ℕ) : (⇑Polynomial.derivative)^[k] (Polynomial.X ^ n) = Polynomial.C ↑(Nat.descFactorial n 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) = ↑(Nat.descFactorial n 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) = Nat.descFactorial n 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 (Polynomial.comp p q) = Polynomial.derivative q * Polynomial.comp (Polynomial.derivative p) 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.prod (Multiset.map f s)) = Multiset.sum (Multiset.map (fun (i : ι) => Multiset.prod (Multiset.map f (Multiset.erase s i)) * Polynomial.derivative (f i)) s)

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

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

@[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

theorem Polynomial.derivative_comp_one_sub_X {R : Type u} [CommRing R] (p : Polynomial R) : Polynomial.derivative (Polynomial.comp p (1 - Polynomial.X)) = -Polynomial.comp (Polynomial.derivative p) (1 - Polynomial.X)

@[simp]

theorem Polynomial.iterate_derivative_comp_one_sub_X {R : Type u} [CommRing R] (p : Polynomial R) (k : ℕ) : (⇑Polynomial.derivative)^[k] (Polynomial.comp p (1 - Polynomial.X)) = (-1) ^ k * Polynomial.comp ((⇑Polynomial.derivative)^[k] p) (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.prod (Multiset.map (fun (a : R) => Polynomial.X - Polynomial.C a) S))) = Multiset.prod (Multiset.map (fun (a : R) => r - a) (Multiset.erase S r))

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) = Nat.descFactorial n 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) = ↑(Nat.factorial n)