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.pderivative i p: the partial derivative ofpwith respect toi.
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^sa : Ri : σ, with corresponding monomialX i, often denotedX_iby mathematiciansp : mv_polynomial σ R
def
mv_polynomial.pderivative
{R : Type u}
{σ : Type u_1}
[comm_semiring R]
(i : σ) :
mv_polynomial σ R →ₗ[R] mv_polynomial σ R
pderivative i p is the partial derivative of p with respect to i
Equations
- mv_polynomial.pderivative i = {to_fun := λ (p : mv_polynomial σ R), finsupp.sum p (λ (A : σ →₀ ℕ) (B : R), mv_polynomial.monomial (A - finsupp.single i 1) (B * ↑(⇑A i))), map_add' := _, map_smul' := _}
@[simp]
theorem
mv_polynomial.pderivative_monomial
{R : Type u}
{σ : Type u_1}
{a : R}
{s : σ →₀ ℕ}
[comm_semiring R]
{i : σ} :
⇑(mv_polynomial.pderivative i) (mv_polynomial.monomial s a) = mv_polynomial.monomial (s - finsupp.single i 1) (a * ↑(⇑s i))
@[simp]
theorem
mv_polynomial.pderivative_C
{R : Type u}
{σ : Type u_1}
{a : R}
[comm_semiring R]
{i : σ} :
⇑(mv_polynomial.pderivative i) (⇑mv_polynomial.C a) = 0
theorem
mv_polynomial.pderivative_eq_zero_of_not_mem_vars
{R : Type u}
{σ : Type u_1}
[comm_semiring R]
{i : σ}
{f : mv_polynomial σ R}
(h : i ∉ f.vars) :
⇑(mv_polynomial.pderivative i) f = 0
theorem
mv_polynomial.pderivative_monomial_single
{R : Type u}
{σ : Type u_1}
{a : R}
[comm_semiring R]
{i : σ}
{n : ℕ} :
⇑(mv_polynomial.pderivative i) (mv_polynomial.monomial (finsupp.single i n) a) = mv_polynomial.monomial (finsupp.single i (n - 1)) (a * ↑n)
theorem
mv_polynomial.pderivative_monomial_mul
{R : Type u}
{σ : Type u_1}
{a a' : R}
{s : σ →₀ ℕ}
[comm_semiring R]
{i : σ}
{s' : σ →₀ ℕ} :
⇑(mv_polynomial.pderivative i) ((mv_polynomial.monomial s a) * mv_polynomial.monomial s' a') = (⇑(mv_polynomial.pderivative i) (mv_polynomial.monomial s a)) * mv_polynomial.monomial s' a' + (mv_polynomial.monomial s a) * ⇑(mv_polynomial.pderivative i) (mv_polynomial.monomial s' a')
@[simp]
theorem
mv_polynomial.pderivative_mul
{R : Type u}
{σ : Type u_1}
[comm_semiring R]
{i : σ}
{f g : mv_polynomial σ R} :
⇑(mv_polynomial.pderivative i) (f * g) = (⇑(mv_polynomial.pderivative i) f) * g + f * ⇑(mv_polynomial.pderivative i) g
@[simp]
theorem
mv_polynomial.pderivative_C_mul
{R : Type u}
{σ : Type u_1}
{a : R}
[comm_semiring R]
{f : mv_polynomial σ R}
{i : σ} :
⇑(mv_polynomial.pderivative i) ((⇑mv_polynomial.C a) * f) = (⇑mv_polynomial.C a) * ⇑(mv_polynomial.pderivative i) f