multivariate chain rule for polynomials

Stream: Is there code for X?

[Junyan Xu]

Is there any form of multivariate chain rule for polynomials in mathlib? We have the analytic version docs#has_fderiv_at.comp which is stated using composition of linear maps.

Here are two versions of 2-variable chain rule in a polynomial ring over a polynomial ring R[X][X], and I'll use Y to refer to the second X. For p : R[X][X] and q : R[X], eval q p means plugging Y := q(X) into p(X,Y); p.derivative is the derivative w.r.t. Y, and p.sum $ λ n r, C r.derivative * X ^ n is the derivative w.r.t. X; I wonder if there's a more idiomatic spelling for the latter. It's very much like docs#polynomial.map but with f := derivative a linear_map instead of a ring_hom.

import data.polynomial.derivative

open_locale polynomial
open polynomial

example {R} [comm_semiring R] (p : R[X][X]) (q : R[X]) : (eval q p).derivative =
  p.sum (λ n r, r.derivative * q ^ n) + q.derivative * eval q p.derivative :=
sorry

example {R} [comm_semiring R] (p : R[X][X]) (q : R[X]) : (eval q p).derivative =
  eval q (p.sum $ λ n r, C r.derivative * X ^ n) + q.derivative * eval q p.derivative :=
sorry

[Junyan Xu]

and here are statements using genuine mv_polynomials. Are there better suggestions?

import data.mv_polynomial.pderiv

open mv_polynomial
open_locale polynomial

example {σ R} [comm_semiring R] (f : σ → R[X]) (p : mv_polynomial σ R) :
  (eval₂ (@polynomial.C R _) f p).derivative =
  p.vars.sum (λ i, (f i).derivative * eval₂ polynomial.C f (pderiv i p)) := sorry

example {σ R} [fintype σ] [comm_semiring R] (f : σ → R[X]) (p : mv_polynomial σ R) :
  (eval₂ (@polynomial.C R _) f p).derivative =
  finset.univ.sum (λ i, (f i).derivative * eval₂ polynomial.C f (pderiv i p)) := sorry

[David Ang]

I just saw this - I'm wondering the same thing i.e. if it's possible to map the linear map derivative across a polynomial

[Junyan Xu]

Notice that there is docs#finsupp.map_range.linear_map and docs#polynomial is a wrapper around finsupp.