Partial derivatives of polynomials #

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

This file defines the notion of the formal partial derivative of a polynomial, the derivative with respect to a single variable. This derivative is not connected to the notion of derivative from analysis. It is based purely on the polynomial exponents and coefficients.

Main declarations #

mv_polynomial.pderiv i p : the partial derivative of p with respect to i, as a bundled derivation of mv_polynomial σ R.

Notation #

As in other polynomial files, we typically use the notation:

σ : Type* (indexing the variables)
R : Type* [comm_ring R] (the coefficients)
s : σ →₀ ℕ, a function from σ to ℕ which is zero away from a finite set. This will give rise to a monomial in mv_polynomial σ R which mathematicians might call X^s
a : R
i : σ, with corresponding monomial X i, often denoted X_i by mathematicians
p : mv_polynomial σ R

source

noncomputable def mv_polynomial.pderiv {R : Type u} {σ : Type v} [comm_semiring R] (i : σ) :

derivation R (mv_polynomial σ R) (mv_polynomial σ R)

pderiv i p is the partial derivative of p with respect to i

Equations

mv_polynomial.pderiv i = let _inst : decidable_eq σ := classical.dec_eq σ in mv_polynomial.mk_derivation R (pi.single i 1)

source

theorem mv_polynomial.pderiv_def {R : Type u} {σ : Type v} [comm_semiring R] [decidable_eq σ] (i : σ) :

mv_polynomial.pderiv i = mv_polynomial.mk_derivation R (pi.single i 1)

source

@[simp]

theorem mv_polynomial.pderiv_monomial {R : Type u} {σ : Type v} {a : R} {s : σ →₀ ℕ} [comm_semiring R] {i : σ} :

⇑(mv_polynomial.pderiv i) (⇑(mv_polynomial.monomial s) a) = ⇑(mv_polynomial.monomial (s - finsupp.single i 1)) (a * ↑(⇑s i))

source

theorem mv_polynomial.pderiv_C {R : Type u} {σ : Type v} {a : R} [comm_semiring R] {i : σ} :

⇑(mv_polynomial.pderiv i) (⇑mv_polynomial.C a) = 0

source

theorem mv_polynomial.pderiv_one {R : Type u} {σ : Type v} [comm_semiring R] {i : σ} :

⇑(mv_polynomial.pderiv i) 1 = 0

source

@[simp]

theorem mv_polynomial.pderiv_X {R : Type u} {σ : Type v} [comm_semiring R] [decidable_eq σ] (i j : σ) :

⇑(mv_polynomial.pderiv i) (mv_polynomial.X j) = pi.single i 1 j

source

@[simp]

theorem mv_polynomial.pderiv_X_self {R : Type u} {σ : Type v} [comm_semiring R] (i : σ) :

⇑(mv_polynomial.pderiv i) (mv_polynomial.X i) = 1

source

@[simp]

theorem mv_polynomial.pderiv_X_of_ne {R : Type u} {σ : Type v} [comm_semiring R] {i j : σ} (h : j ≠ i) :

⇑(mv_polynomial.pderiv i) (mv_polynomial.X j) = 0

source

theorem mv_polynomial.pderiv_eq_zero_of_not_mem_vars {R : Type u} {σ : Type v} [comm_semiring R] {i : σ} {f : mv_polynomial σ R} (h : i ∉ f.vars) :

⇑(mv_polynomial.pderiv i) f = 0

source

theorem mv_polynomial.pderiv_monomial_single {R : Type u} {σ : Type v} {a : R} [comm_semiring R] {i : σ} {n : ℕ} :

⇑(mv_polynomial.pderiv i) (⇑(mv_polynomial.monomial (finsupp.single i n)) a) = ⇑(mv_polynomial.monomial (finsupp.single i (n - 1))) (a * ↑n)

source

theorem mv_polynomial.pderiv_mul {R : Type u} {σ : Type v} [comm_semiring R] {i : σ} {f g : mv_polynomial σ R} :

⇑(mv_polynomial.pderiv i) (f * g) = ⇑(mv_polynomial.pderiv i) f * g + f * ⇑(mv_polynomial.pderiv i) g

source

@[simp]

theorem mv_polynomial.pderiv_C_mul {R : Type u} {σ : Type v} {a : R} [comm_semiring R] {f : mv_polynomial σ R} {i : σ} :

⇑(mv_polynomial.pderiv i) (⇑mv_polynomial.C a * f) = ⇑mv_polynomial.C a * ⇑(mv_polynomial.pderiv i) f