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))
@[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]
@[simp]
@[simp]
@[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
@[simp]
theorem
polynomial.iterate_derivative_smul
{R : Type u}
[semiring R]
(r : R)
(p : polynomial R)
(k : ℕ) :
@[simp]
theorem
polynomial.derivative_C_mul
{R : Type u}
[semiring R]
(a : R)
(p : polynomial R) :
⇑polynomial.derivative ((⇑polynomial.C a) * p) = (⇑polynomial.C a) * ⇑polynomial.derivative p
We can't use derivative_mul
here because
we want to prove this statement also for noncommutative rings.
@[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.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_comp
{R : Type u}
[comm_semiring R]
(p q : polynomial R) :
⇑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 : polynomial R)
(f : R →+* S) :
@[simp]
theorem
polynomial.iterate_derivative_map
{R : Type u}
{S : Type v}
[comm_semiring R]
[comm_semiring S]
(p : polynomial R)
(f : R →+* S)
(k : ℕ) :
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
The formal derivative of polynomials, as linear homomorphism.
Equations
- polynomial.derivative_lhom R = {to_fun := ⇑polynomial.derivative, map_add' := _, map_smul' := _}
@[simp]
@[simp]
@[simp]
theorem
polynomial.iterate_derivative_cast_nat_mul
{R : Type u}
[comm_semiring R]
{n k : ℕ}
{f : polynomial R} :
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)
@[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)
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