The derivative map on polynomials #
Main definitions #
polynomial.derivative: The formal derivative of polynomials, expressed as a linear map.
derivative p is the formal derivative of the polynomial p
theorem
polynomial.derivative_apply
{R : Type u}
[semiring R]
(p : R[X]) :
⇑polynomial.derivative p = p.sum (λ (n : ℕ) (a : R), (⇑polynomial.C (a * ↑n)) * polynomial.X ^ (n - 1))
@[simp]
@[simp]
@[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_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)
@[simp]
theorem
polynomial.derivative_X_pow
{R : Type u}
[semiring R]
(n : ℕ) :
⇑polynomial.derivative (polynomial.X ^ n) = (↑n) * polynomial.X ^ (n - 1)
@[simp]
theorem
polynomial.derivative_of_nat_degree_zero
{R : Type u}
[semiring R]
{p : R[X]}
(hp : p.nat_degree = 0) :
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
polynomial.derivative_sum
{R : Type u}
{ι : Type y}
[semiring R]
{s : finset ι}
{f : ι → R[X]} :
⇑polynomial.derivative (∑ (b : ι) in s, f b) = ∑ (b : ι) in s, ⇑polynomial.derivative (f b)
@[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 : R[X]) :
⇑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]
[distrib_mul_action S R]
[is_scalar_tower S R R]
(s : S)
(p : R[X])
(k : ℕ) :
@[simp]
theorem
polynomial.iterate_derivative_C_mul
{R : Type u}
[semiring R]
(a : R)
(p : R[X])
(k : ℕ) :
⇑polynomial.derivative^[k] ((⇑polynomial.C a) * p) = (⇑polynomial.C a) * ⇑polynomial.derivative^[k] p
theorem
polynomial.degree_derivative_lt
{R : Type u}
[semiring R]
{p : R[X]}
(hp : p ≠ 0) :
(⇑polynomial.derivative p).degree < p.degree
theorem
polynomial.degree_derivative_le
{R : Type u}
[semiring R]
{p : R[X]} :
(⇑polynomial.derivative p).degree ≤ p.degree
theorem
polynomial.nat_degree_derivative_lt
{R : Type u}
[semiring R]
{p : R[X]}
(hp : p.nat_degree ≠ 0) :
theorem
polynomial.nat_degree_derivative_le
{R : Type u}
[semiring R]
(p : R[X]) :
(⇑polynomial.derivative p).nat_degree ≤ p.nat_degree - 1
@[simp]
theorem
polynomial.iterate_derivative_eq_zero
{R : Type u}
[semiring R]
{p : R[X]}
{x : ℕ}
(hx : p.nat_degree < x) :
theorem
polynomial.nat_degree_eq_zero_of_derivative_eq_zero
{R : Type u}
[semiring R]
[no_zero_divisors R]
[char_zero R]
{f : R[X]}
(h : ⇑polynomial.derivative f = 0) :
f.nat_degree = 0
@[simp]
theorem
polynomial.derivative_mul
{R : Type u}
[semiring R]
{f g : R[X]} :
⇑polynomial.derivative (f * g) = (⇑polynomial.derivative f) * g + f * ⇑polynomial.derivative g
theorem
polynomial.derivative_comp
{R : Type u}
[comm_semiring R]
(p q : R[X]) :
⇑polynomial.derivative (p.comp q) = (⇑polynomial.derivative q) * (⇑polynomial.derivative p).comp q
@[simp]
theorem
polynomial.derivative_map
{R : Type u}
{S : Type v}
[comm_semiring R]
[comm_semiring S]
(p : R[X])
(f : R →+* S) :
@[simp]
theorem
polynomial.iterate_derivative_map
{R : Type u}
{S : Type v}
[comm_semiring R]
[comm_semiring S]
(p : R[X])
(f : R →+* S)
(k : ℕ) :
Chain rule for formal derivative of polynomials.
theorem
polynomial.derivative_prod
{R : Type u}
{ι : Type y}
[comm_semiring R]
{s : multiset ι}
{f : ι → R[X]} :
⇑polynomial.derivative (multiset.map f s).prod = (multiset.map (λ (i : ι), ((multiset.map f (s.erase i)).prod) * ⇑polynomial.derivative (f i)) s).sum
@[simp]
theorem
polynomial.iterate_derivative_cast_nat_mul
{R : Type u}
[comm_semiring R]
{n k : ℕ}
{f : R[X]} :
@[simp]
@[simp]
@[simp]
theorem
polynomial.derivative_comp_one_sub_X
{R : Type u}
[comm_ring R]
(p : R[X]) :
⇑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}
[comm_ring R]
(p : R[X])
(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}
[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
theorem
polynomial.mem_support_derivative
{R : Type u}
[ring R]
[no_zero_divisors R]
[char_zero R]
(p : R[X])
(n : ℕ) :
@[simp]
theorem
polynomial.degree_derivative_eq
{R : Type u}
[ring R]
[no_zero_divisors R]
[char_zero R]
(p : R[X])
(hp : 0 < p.nat_degree) :
(⇑polynomial.derivative p).degree = ↑(p.nat_degree - 1)