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
Equations
- polynomial.derivative = finsupp.total ℕ (polynomial R) R (λ (n : ℕ), (⇑polynomial.C ↑n) * polynomial.X ^ (n - 1))
theorem
polynomial.derivative_apply
{R : Type u}
[semiring R]
(p : polynomial R) :
⇑polynomial.derivative p = finsupp.sum p (λ (n : ℕ) (a : R), (⇑polynomial.C (a * ↑n)) * polynomial.X ^ (n - 1))
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]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
polynomial.derivative_sum
{R : Type u}
{ι : Type y}
[semiring R]
{s : finset ι}
{f : ι → polynomial R} :
⇑polynomial.derivative (∑ (b : ι) in s, f b) = ∑ (b : ι) in s, ⇑polynomial.derivative (f b)
@[simp]
theorem
polynomial.derivative_smul
{R : Type u}
[semiring R]
(r : R)
(p : polynomial R) :
⇑polynomial.derivative (r • p) = r • ⇑polynomial.derivative p
theorem
polynomial.derivative_eval
{R : Type u}
[comm_semiring R]
(p : polynomial R)
(x : R) :
polynomial.eval x (⇑polynomial.derivative p) = finsupp.sum p (λ (n : ℕ) (a : R), (a * ↑n) * x ^ (n - 1))
@[simp]
theorem
polynomial.derivative_mul
{R : Type u}
[comm_semiring R]
{f g : polynomial R} :
⇑polynomial.derivative (f * g) = (⇑polynomial.derivative f) * g + f * ⇑polynomial.derivative g
theorem
polynomial.derivative_map
{R : Type u}
{S : Type v}
[comm_semiring R]
[comm_semiring S]
(p : polynomial R)
(f : R →+* S) :
Chain rule for formal derivative of polynomials.
theorem
polynomial.of_mem_support_derivative
{R : Type u}
[comm_semiring R]
{p : polynomial R}
{n : ℕ}
(h : n ∈ (⇑polynomial.derivative p).support) :
theorem
polynomial.degree_derivative_lt
{R : Type u}
[comm_semiring R]
{p : polynomial R}
(hp : p ≠ 0) :
(⇑polynomial.derivative p).degree < p.degree
theorem
polynomial.nat_degree_derivative_lt
{R : Type u}
[comm_semiring R]
{p : polynomial R}
(hp : ⇑polynomial.derivative p ≠ 0) :
theorem
polynomial.degree_derivative_le
{R : Type u}
[comm_semiring R]
{p : polynomial R} :
(⇑polynomial.derivative p).degree ≤ p.degree
theorem
polynomial.mem_support_derivative
{R : Type u}
[integral_domain R]
[char_zero R]
(p : polynomial R)
(n : ℕ) :
@[simp]
theorem
polynomial.degree_derivative_eq
{R : Type u}
[integral_domain R]
[char_zero R]
(p : polynomial R)
(hp : 0 < p.nat_degree) :
(⇑polynomial.derivative p).degree = ↑(p.nat_degree - 1)
theorem
polynomial.nat_degree_eq_zero_of_derivative_eq_zero
{R : Type u}
[integral_domain R]
[char_zero R]
{f : polynomial R}
(h : ⇑polynomial.derivative f = 0) :
f.nat_degree = 0