Partial derivatives of polynomials #
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 ofpwith respect toi, as a bundled derivation ofmv_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 inmv_polynomial σ Rwhich mathematicians might callX^s -
a : R -
i : σ, with corresponding monomialX i, often denotedX_iby mathematicians -
p : mv_polynomial σ R
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
@[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))
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
theorem
mv_polynomial.pderiv_one
{R : Type u}
{σ : Type v}
[comm_semiring R]
{i : σ} :
⇑(mv_polynomial.pderiv i) 1 = 0
@[simp]
theorem
mv_polynomial.pderiv_X
{R : Type u}
{σ : Type v}
[comm_semiring R]
[d : decidable_eq σ]
(i j : σ) :
⇑(mv_polynomial.pderiv i) (mv_polynomial.X j) = pi.single i 1 j
@[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
@[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
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
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)
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
@[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