mathlib3 documentation

data.polynomial.derivative

The derivative map on polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main definitions #

source
noncomputable def polynomial.derivative {R : Type u} [semiring R] :
polynomial R →ₗ[R] polynomial R

derivative p is the formal derivative of the polynomial p

Equations
source
theorem polynomial.derivative_apply {R : Type u} [semiring R] (p : polynomial R) :
⇑polynomial.derivative p = p.sum (λ (n : ℕ) (a : R), ⇑polynomial.C (a * ↑n) * polynomial.X ^ (n - 1))
source
theorem polynomial.coeff_derivative {R : Type u} [semiring R] (p : polynomial R) (n : ℕ) :
(⇑polynomial.derivative p).coeff n = p.coeff (n + 1) * (↑n + 1)
source
@[simp]
theorem polynomial.derivative_zero {R : Type u} [semiring R] :
⇑polynomial.derivative 0 = 0
source
@[simp]
theorem polynomial.iterate_derivative_zero {R : Type u} [semiring R] {k : ℕ} :
⇑polynomial.derivative^[k] 0 = 0
source
@[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)
source
theorem polynomial.derivative_C_mul_X {R : Type u} [semiring R] (a : R) :
⇑polynomial.derivative (⇑polynomial.C a * polynomial.X) = ⇑polynomial.C a
source
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)
source
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
source
@[simp]
theorem polynomial.derivative_X_pow {R : Type u} [semiring R] (n : ℕ) :
⇑polynomial.derivative (polynomial.X ^ n) = ⇑polynomial.C ↑n * polynomial.X ^ (n - 1)
source
@[simp]
theorem polynomial.derivative_X_sq {R : Type u} [semiring R] :
⇑polynomial.derivative (polynomial.X ^ 2) = ⇑polynomial.C 2 * polynomial.X
source
@[simp]
theorem polynomial.derivative_C {R : Type u} [semiring R] {a : R} :
⇑polynomial.derivative (⇑polynomial.C a) = 0
source
theorem polynomial.derivative_of_nat_degree_zero {R : Type u} [semiring R] {p : polynomial R} (hp : p.nat_degree = 0) :
⇑polynomial.derivative p = 0
source
@[simp]
theorem polynomial.derivative_X {R : Type u} [semiring R] :
⇑polynomial.derivative polynomial.X = 1
source
@[simp]
theorem polynomial.derivative_one {R : Type u} [semiring R] :
⇑polynomial.derivative 1 = 0
source
@[simp]
theorem polynomial.derivative_bit0 {R : Type u} [semiring R] {a : polynomial R} :
⇑polynomial.derivative (bit0 a) = bit0 (⇑polynomial.derivative a)
source
@[simp]
theorem polynomial.derivative_bit1 {R : Type u} [semiring R] {a : polynomial R} :
⇑polynomial.derivative (bit1 a) = bit0 (⇑polynomial.derivative a)
source
@[simp]
theorem polynomial.derivative_add {R : Type u} [semiring R] {f g : polynomial R} :
⇑polynomial.derivative (f + g) = ⇑polynomial.derivative f + ⇑polynomial.derivative g
source
@[simp]
theorem polynomial.derivative_X_add_C {R : Type u} [semiring R] (c : R) :
⇑polynomial.derivative (polynomial.X + ⇑polynomial.C c) = 1
source
@[simp]
theorem polynomial.iterate_derivative_add {R : Type u} [semiring R] {f g : polynomial R} {k : ℕ} :
⇑polynomial.derivative^[k] (f + g) = ⇑polynomial.derivative^[k] f + ⇑polynomial.derivative^[k] g
source
@[simp]
theorem polynomial.derivative_sum {R : Type u} {ι : Type y} [semiring R] {s : finset ι} {f : ι → polynomial R} :
⇑polynomial.derivative (s.sum (λ (b : ι), f b)) = s.sum (λ (b : ι), ⇑polynomial.derivative (f b))
source
@[simp]
theorem polynomial.derivative_smul {R : Type u} [semiring R] {S : Type u_1} [monoid S] [distrib_mul_action S R] [is_scalar_tower S R R] (s : S) (p : polynomial R) :
⇑polynomial.derivative (s • p) = s • ⇑polynomial.derivative p
source
@[simp]
theorem polynomial.iterate_derivative_smul {R : Type u} [semiring R] {S : Type u_1} [monoid S] [distrib_mul_action S R] [is_scalar_tower S R R] (s : S) (p : polynomial R) (k : ℕ) :
⇑polynomial.derivative^[k] (s • p) = s • ⇑polynomial.derivative^[k] p
source
@[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
source
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
source
theorem polynomial.degree_derivative_lt {R : Type u} [semiring R] {p : polynomial R} (hp : p ≠ 0) :
(⇑polynomial.derivative p).degree < p.degree
source
theorem polynomial.degree_derivative_le {R : Type u} [semiring R] {p : polynomial R} :
(⇑polynomial.derivative p).degree ≤ p.degree
source
theorem polynomial.nat_degree_derivative_lt {R : Type u} [semiring R] {p : polynomial R} (hp : p.nat_degree ≠ 0) :
(⇑polynomial.derivative p).nat_degree < p.nat_degree
source
theorem polynomial.nat_degree_derivative_le {R : Type u} [semiring R] (p : polynomial R) :
(⇑polynomial.derivative p).nat_degree ≤ p.nat_degree - 1
source
@[simp]
theorem polynomial.derivative_nat_cast {R : Type u} [semiring R] {n : ℕ} :
⇑polynomial.derivative ↑n = 0
source
theorem polynomial.iterate_derivative_eq_zero {R : Type u} [semiring R] {p : polynomial R} {x : ℕ} (hx : p.nat_degree < x) :
⇑polynomial.derivative^[x] p = 0
source
@[simp]
theorem polynomial.iterate_derivative_C {R : Type u} {a : R} [semiring R] {k : ℕ} (h : 0 < k) :
⇑polynomial.derivative^[k] (⇑polynomial.C a) = 0
source
@[simp]
theorem polynomial.iterate_derivative_one {R : Type u} [semiring R] {k : ℕ} (h : 0 < k) :
⇑polynomial.derivative^[k] 1 = 0
source
@[simp]
theorem polynomial.iterate_derivative_X {R : Type u} [semiring R] {k : ℕ} (h : 1 < k) :
⇑polynomial.derivative^[k] polynomial.X = 0
source
theorem polynomial.nat_degree_eq_zero_of_derivative_eq_zero {R : Type u} [semiring R] [no_zero_smul_divisors ℕ R] {f : polynomial R} (h : ⇑polynomial.derivative f = 0) :
f.nat_degree = 0
source
theorem polynomial.eq_C_of_derivative_eq_zero {R : Type u} [semiring R] [no_zero_smul_divisors ℕ R] {f : polynomial R} (h : ⇑polynomial.derivative f = 0) :
f = ⇑polynomial.C (f.coeff 0)
source
@[simp]
theorem polynomial.derivative_mul {R : Type u} [semiring R] {f g : polynomial R} :
⇑polynomial.derivative (f * g) = ⇑polynomial.derivative f * g + f * ⇑polynomial.derivative g
source
theorem polynomial.derivative_eval {R : Type u} [semiring R] (p : polynomial R) (x : R) :
polynomial.eval x (⇑polynomial.derivative p) = p.sum (λ (n : ℕ) (a : R), a * ↑n * x ^ (n - 1))
source
@[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)
source
@[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)
source
theorem polynomial.derivative_nat_cast_mul {R : Type u} [semiring R] {n : ℕ} {f : polynomial R} :
⇑polynomial.derivative (↑n * f) = ↑n * ⇑polynomial.derivative f
source
@[simp]
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
source
theorem polynomial.mem_support_derivative {R : Type u} [semiring R] [no_zero_smul_divisors ℕ R] (p : polynomial R) (n : ℕ) :
n ∈ (⇑polynomial.derivative p).support ↔ n + 1 ∈ p.support
source
@[simp]
theorem polynomial.degree_derivative_eq {R : Type u} [semiring R] [no_zero_smul_divisors ℕ R] (p : polynomial R) (hp : 0 < p.nat_degree) :
(⇑polynomial.derivative p).degree = ↑(p.nat_degree - 1)
source
theorem polynomial.coeff_iterate_derivative_as_prod_Ico {R : Type u} [semiring R] {k : ℕ} (p : polynomial R) (m : ℕ) :
(⇑polynomial.derivative^[k] p).coeff m = (finset.Ico m.succ (m + k.succ)).prod (λ (i : ℕ), i) • p.coeff (m + k)
source
theorem polynomial.coeff_iterate_derivative_as_prod_range {R : Type u} [semiring R] {k : ℕ} (p : polynomial R) (m : ℕ) :
(⇑polynomial.derivative^[k] p).coeff m = (finset.range k).prod (λ (i : ℕ), m + k - i) • p.coeff (m + k)
source
theorem polynomial.iterate_derivative_mul {R : Type u} [semiring R] {n : ℕ} (p q : polynomial R) :
⇑polynomial.derivative^[n] (p * q) = (finset.range n.succ).sum (λ (k : ℕ), n.choose k • (⇑polynomial.derivative^[n - k] p * ⇑polynomial.derivative^[k] q))
source
theorem polynomial.derivative_pow_succ {R : Type u} [comm_semiring R] (p : polynomial R) (n : ℕ) :
⇑polynomial.derivative (p ^ (n + 1)) = ⇑polynomial.C ↑(n + 1) * p ^ n * ⇑polynomial.derivative p
source
theorem polynomial.derivative_pow {R : Type u} [comm_semiring R] (p : polynomial R) (n : ℕ) :
⇑polynomial.derivative (p ^ n) = ⇑polynomial.C ↑n * p ^ (n - 1) * ⇑polynomial.derivative p
source
theorem polynomial.derivative_sq {R : Type u} [comm_semiring R] (p : polynomial R) :
⇑polynomial.derivative (p ^ 2) = ⇑polynomial.C 2 * p * ⇑polynomial.derivative p
source
theorem polynomial.dvd_iterate_derivative_pow {R : Type u} [comm_semiring R] (f : polynomial R) (n : ℕ) {m : ℕ} (c : R) (hm : m ≠ 0) :
↑n ∣ polynomial.eval c (⇑polynomial.derivative^[m] (f ^ n))
source
theorem polynomial.iterate_derivative_X_pow_eq_nat_cast_mul {R : Type u} [comm_semiring R] (n k : ℕ) :
⇑polynomial.derivative^[k] (polynomial.X ^ n) = ↑(n.desc_factorial k) * polynomial.X ^ (n - k)
source
theorem polynomial.iterate_derivative_X_pow_eq_C_mul {R : Type u} [comm_semiring R] (n k : ℕ) :
⇑polynomial.derivative^[k] (polynomial.X ^ n) = ⇑polynomial.C ↑(n.desc_factorial k) * polynomial.X ^ (n - k)
source
theorem polynomial.iterate_derivative_X_pow_eq_smul {R : Type u} [comm_semiring R] (n k : ℕ) :
⇑polynomial.derivative^[k] (polynomial.X ^ n) = ↑(n.desc_factorial k) • polynomial.X ^ (n - k)
source
theorem polynomial.derivative_X_add_C_pow {R : Type u} [comm_semiring R] (c : R) (m : ℕ) :
⇑polynomial.derivative ((polynomial.X + ⇑polynomial.C c) ^ m) = ⇑polynomial.C ↑m * (polynomial.X + ⇑polynomial.C c) ^ (m - 1)
source
theorem polynomial.derivative_X_add_C_sq {R : Type u} [comm_semiring R] (c : R) :
⇑polynomial.derivative ((polynomial.X + ⇑polynomial.C c) ^ 2) = ⇑polynomial.C 2 * (polynomial.X + ⇑polynomial.C c)
source
theorem polynomial.iterate_derivative_X_add_pow {R : Type u} [comm_semiring R] (n k : ℕ) (c : R) :
⇑polynomial.derivative^[k] ((polynomial.X + ⇑polynomial.C c) ^ n) = ↑((finset.range k).prod (λ (i : ℕ), n - i)) * (polynomial.X + ⇑polynomial.C c) ^ (n - k)
source
theorem polynomial.derivative_comp {R : Type u} [comm_semiring R] (p q : polynomial R) :
⇑polynomial.derivative (p.comp q) = ⇑polynomial.derivative q * (⇑polynomial.derivative p).comp q
source
theorem polynomial.derivative_eval₂_C {R : Type u} [comm_semiring R] (p 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.

source
theorem polynomial.derivative_prod {R : Type u} {ι : Type y} [comm_semiring R] {s : multiset ι} {f : ι → polynomial R} :
⇑polynomial.derivative (multiset.map f s).prod = (multiset.map (λ (i : ι), (multiset.map f (s.erase i)).prod * ⇑polynomial.derivative (f i)) s).sum
source
@[simp]
theorem polynomial.derivative_neg {R : Type u} [ring R] (f : polynomial R) :
⇑polynomial.derivative (-f) = -⇑polynomial.derivative f
source
@[simp]
theorem polynomial.iterate_derivative_neg {R : Type u} [ring R] {f : polynomial R} {k : ℕ} :
⇑polynomial.derivative^[k] (-f) = -⇑polynomial.derivative^[k] f
source
@[simp]
theorem polynomial.derivative_sub {R : Type u} [ring R] {f g : polynomial R} :
⇑polynomial.derivative (f - g) = ⇑polynomial.derivative f - ⇑polynomial.derivative g
source
@[simp]
theorem polynomial.derivative_X_sub_C {R : Type u} [ring R] (c : R) :
⇑polynomial.derivative (polynomial.X - ⇑polynomial.C c) = 1
source
@[simp]
theorem polynomial.iterate_derivative_sub {R : Type u} [ring R] {k : ℕ} {f g : polynomial R} :
⇑polynomial.derivative^[k] (f - g) = ⇑polynomial.derivative^[k] f - ⇑polynomial.derivative^[k] g
source
@[simp]
theorem polynomial.derivative_int_cast {R : Type u} [ring R] {n : ℤ} :
⇑polynomial.derivative ↑n = 0
source
theorem polynomial.derivative_int_cast_mul {R : Type u} [ring R] {n : ℤ} {f : polynomial R} :
⇑polynomial.derivative (↑n * f) = ↑n * ⇑polynomial.derivative f
source
@[simp]
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
source
theorem polynomial.derivative_comp_one_sub_X {R : Type u} [comm_ring R] (p : polynomial R) :
⇑polynomial.derivative (p.comp (1 - polynomial.X)) = -(⇑polynomial.derivative p).comp (1 - polynomial.X)
source
@[simp]
theorem polynomial.iterate_derivative_comp_one_sub_X {R : Type u} [comm_ring R] (p : polynomial R) (k : ℕ) :
⇑polynomial.derivative^[k] (p.comp (1 - polynomial.X)) = (-1) ^ k * (⇑polynomial.derivative^[k] p).comp (1 - polynomial.X)
source
theorem polynomial.eval_multiset_prod_X_sub_C_derivative {R : Type u} [comm_ring R] {S : multiset R} {r : R} (hr : r ∈ S) :
polynomial.eval r (⇑polynomial.derivative (multiset.map (λ (a : R), polynomial.X - ⇑polynomial.C a) S).prod) = (multiset.map (λ (a : R), r - a) (S.erase r)).prod
source
theorem polynomial.derivative_X_sub_C_pow {R : Type u} [comm_ring R] (c : R) (m : ℕ) :
⇑polynomial.derivative ((polynomial.X - ⇑polynomial.C c) ^ m) = ⇑polynomial.C ↑m * (polynomial.X - ⇑polynomial.C c) ^ (m - 1)
source
theorem polynomial.derivative_X_sub_C_sq {R : Type u} [comm_ring R] (c : R) :
⇑polynomial.derivative ((polynomial.X - ⇑polynomial.C c) ^ 2) = ⇑polynomial.C 2 * (polynomial.X - ⇑polynomial.C c)
source
theorem polynomial.iterate_derivative_X_sub_pow {R : Type u} [comm_ring R] (n k : ℕ) (c : R) :
⇑polynomial.derivative^[k] ((polynomial.X - ⇑polynomial.C c) ^ n) = ↑((finset.range k).prod (λ (i : ℕ), n - i)) * (polynomial.X - ⇑polynomial.C c) ^ (n - k)