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

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

Notation

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

• σ : Type* (indexing the variables)

• R : Type* [CommRing R] (the coefficients)

• s : σ →₀ ℕ, a function from σ to ℕ which is zero away from a finite set. This will give rise to a monomial in MvPolynomial σ R which mathematicians might call X^s

• a : R

• i : σ, with corresponding monomial X i, often denoted X_i by mathematicians

• p : MvPolynomial σ R

def MvPolynomial.pderiv {R : Type u} {σ : Type v} [CommSemiring R] (i : σ) : Derivation R (MvPolynomial σ R) (MvPolynomial σ R)

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

Equations

• MvPolynomial.pderiv i = MvPolynomial.mkDerivation R (Pi.single i 1)

theorem MvPolynomial.pderiv_def {R : Type u} {σ : Type v} [CommSemiring R] [DecidableEq σ] (i : σ) : MvPolynomial.pderiv i = MvPolynomial.mkDerivation R (Pi.single i 1)

@[simp]

theorem MvPolynomial.pderiv_monomial {R : Type u} {σ : Type v} {a : R} {s : σ →₀ ℕ} [CommSemiring R] {i : σ} : (MvPolynomial.pderiv i) ((MvPolynomial.monomial s) a) = (MvPolynomial.monomial (s - Finsupp.single i 1)) (a * ↑(s i))

theorem MvPolynomial.X_mul_pderiv_monomial {R : Type u} {σ : Type v} [CommSemiring R] {i : σ} {m : σ →₀ ℕ} {r : R} : MvPolynomial.X i * (MvPolynomial.pderiv i) ((MvPolynomial.monomial m) r) = m i • (MvPolynomial.monomial m) r

theorem MvPolynomial.pderiv_C {R : Type u} {σ : Type v} {a : R} [CommSemiring R] {i : σ} : (MvPolynomial.pderiv i) (MvPolynomial.C a) = 0

theorem MvPolynomial.pderiv_one {R : Type u} {σ : Type v} [CommSemiring R] {i : σ} : (MvPolynomial.pderiv i) 1 = 0

@[simp]

theorem MvPolynomial.pderiv_X {R : Type u} {σ : Type v} [CommSemiring R] [DecidableEq σ] (i j : σ) : (MvPolynomial.pderiv i) (MvPolynomial.X j) = Pi.single i 1 j

@[simp]

theorem MvPolynomial.pderiv_X_self {R : Type u} {σ : Type v} [CommSemiring R] (i : σ) : (MvPolynomial.pderiv i) (MvPolynomial.X i) = 1

@[simp]

theorem MvPolynomial.pderiv_X_of_ne {R : Type u} {σ : Type v} [CommSemiring R] {i j : σ} (h : j ≠ i) : (MvPolynomial.pderiv i) (MvPolynomial.X j) = 0

theorem MvPolynomial.pderiv_eq_zero_of_not_mem_vars {R : Type u} {σ : Type v} [CommSemiring R] {i : σ} {f : MvPolynomial σ R} (h : i ∉ f.vars) : (MvPolynomial.pderiv i) f = 0

theorem MvPolynomial.pderiv_monomial_single {R : Type u} {σ : Type v} {a : R} [CommSemiring R] {i : σ} {n : ℕ} : (MvPolynomial.pderiv i) ((MvPolynomial.monomial (Finsupp.single i n)) a) = (MvPolynomial.monomial (Finsupp.single i (n - 1))) (a * ↑n)

theorem MvPolynomial.pderiv_mul {R : Type u} {σ : Type v} [CommSemiring R] {i : σ} {f g : MvPolynomial σ R} : (MvPolynomial.pderiv i) (f * g) = (MvPolynomial.pderiv i) f * g + f * (MvPolynomial.pderiv i) g

theorem MvPolynomial.pderiv_pow {R : Type u} {σ : Type v} [CommSemiring R] {i : σ} {f : MvPolynomial σ R} {n : ℕ} : (MvPolynomial.pderiv i) (f ^ n) = ↑n * f ^ (n - 1) * (MvPolynomial.pderiv i) f

theorem MvPolynomial.pderiv_C_mul {R : Type u} {σ : Type v} {a : R} [CommSemiring R] {f : MvPolynomial σ R} {i : σ} : (MvPolynomial.pderiv i) (MvPolynomial.C a * f) = MvPolynomial.C a * (MvPolynomial.pderiv i) f

theorem MvPolynomial.pderiv_map {R : Type u} {σ : Type v} [CommSemiring R] {S : Type u_1} [CommSemiring S] {φ : R →+* S} {f : MvPolynomial σ R} {i : σ} : (MvPolynomial.pderiv i) ((MvPolynomial.map φ) f) = (MvPolynomial.map φ) ((MvPolynomial.pderiv i) f)

theorem MvPolynomial.pderiv_rename {R : Type u} {σ : Type v} [CommSemiring R] {τ : Type u_1} {f : σ → τ} (hf : Function.Injective f) (x : σ) (p : MvPolynomial σ R) : (MvPolynomial.pderiv (f x)) ((MvPolynomial.rename f) p) = (MvPolynomial.rename f) ((MvPolynomial.pderiv x) p)

theorem MvPolynomial.aeval_sum_elim_pderiv_inl {R : Type u} {σ : Type v} [CommSemiring R] {S : Type u_1} {τ : Type u_2} [CommRing S] [Algebra R S] (p : MvPolynomial (σ ⊕ τ) R) (f : τ → S) (j : σ) : (MvPolynomial.aeval (Sum.elim MvPolynomial.X (⇑MvPolynomial.C ∘ f))) ((MvPolynomial.pderiv (Sum.inl j)) p) = (MvPolynomial.pderiv j) ((MvPolynomial.aeval (Sum.elim MvPolynomial.X (⇑MvPolynomial.C ∘ f))) p)