mathlib documentation

data.polynomial.derivative

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

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.coeff_derivative {R : Type u} [semiring R] (p : polynomial R) (n : ℕ) :

(⇑polynomial.derivative p).coeff n = (p.coeff (n + 1)) * (↑n + 1)

theorem polynomial.derivative_zero {R : Type u} [semiring R] :

⇑polynomial.derivative 0 = 0

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_C {R : Type u} [semiring R] {a : R} :

⇑polynomial.derivative (⇑polynomial.C a) = 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

@[simp]

theorem polynomial.derivative_bit0 {R : Type u} [semiring R] {a : polynomial R} :

⇑polynomial.derivative (bit0 a) = bit0 (⇑polynomial.derivative a)

@[simp]

theorem polynomial.derivative_bit1 {R : Type u} [semiring R] {a : polynomial R} :

⇑polynomial.derivative (bit1 a) = bit0 (⇑polynomial.derivative a)

@[simp]

theorem polynomial.derivative_add {R : Type u} [semiring R] {f g : polynomial R} :

⇑polynomial.derivative (f + g) = ⇑polynomial.derivative f + ⇑polynomial.derivative g

@[simp]

theorem polynomial.derivative_neg {R : Type u_1} [ring R] (f : polynomial R) :

⇑polynomial.derivative (-f) = -⇑polynomial.derivative f

@[simp]

theorem polynomial.derivative_sub {R : Type u_1} [ring R] (f g : polynomial R) :

⇑polynomial.derivative (f - g) = ⇑polynomial.derivative f - ⇑polynomial.derivative g

@[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_pow_succ {R : Type u} [comm_semiring R] (p : polynomial R) (n : ℕ) :

⇑polynomial.derivative (p ^ (n + 1)) = ((↑n + 1) * p ^ n) * ⇑polynomial.derivative p

theorem polynomial.derivative_pow {R : Type u} [comm_semiring R] (p : polynomial R) (n : ℕ) :

⇑polynomial.derivative (p ^ n) = ((↑n) * p ^ (n - 1)) * ⇑polynomial.derivative p

theorem polynomial.derivative_map {R : Type u} {S : Type v} [comm_semiring R] [comm_semiring S] (p : polynomial R) (f : R →+* S) :

⇑polynomial.derivative (polynomial.map f p) = polynomial.map f (⇑polynomial.derivative p)

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.

theorem polynomial.of_mem_support_derivative {R : Type u} [comm_semiring R] {p : polynomial R} {n : ℕ} (h : n ∈ (⇑polynomial.derivative p).support) :

n + 1 ∈ 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) :

(⇑polynomial.derivative p).nat_degree < p.nat_degree

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 : ℕ) :

n ∈ (⇑polynomial.derivative p).support ↔ n + 1 ∈ p.support

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