Coefficientwise and outer derivatives of bivariate polynomials, and their compatibility with rational differentiation, for the closed-form criterion.

noncomputable def CCDN.bivariateCoefficientDerivative (F : Type u_1) [CommRing F] : Derivation F (Polynomial (Polynomial F)) (Polynomial (Polynomial F))

Differentiate the inner variable of a bivariate polynomial.

Equations

• CCDN.bivariateCoefficientDerivative F = PolynomialModule.equivPolynomialSelf.compDer Polynomial.derivative'.mapCoeffs

@[simp]

theorem CCDN.coeff_bivariateCoefficientDerivative {F : Type u_1} [CommRing F] (p : Polynomial (Polynomial F)) (n : ℕ) : ((bivariateCoefficientDerivative F) p).coeff n = Polynomial.derivative (p.coeff n)

The n-th outer coefficient of the inner derivative of p is the derivative of the n-th outer coefficient of p.

theorem CCDN.bivariateCoefficientDerivative_monomial {R : Type u_1} [CommRing R] (m n : ℕ) (a : R) : (bivariateCoefficientDerivative R) ((Polynomial.monomial m) ((Polynomial.monomial n) a)) = (Polynomial.monomial m) ((Polynomial.monomial (n - 1)) (a * ↑n))

The inner derivative of the monomial with outer exponent m, inner exponent n and coefficient a is the monomial with exponents m, n - 1 and coefficient a * n.

theorem CCDN.bivariate_derivative_monomial {R : Type u_1} [CommRing R] (m n : ℕ) (a : R) : Polynomial.derivative ((Polynomial.monomial m) ((Polynomial.monomial n) a)) = (Polynomial.monomial (m - 1)) ((Polynomial.monomial n) (a * ↑m))

Differentiate a bivariate monomial in the outer variable.

theorem CCDN.bivariateCoefficientDerivative_map {F : Type u_1} [Field F] (p : Polynomial (Polynomial F)) : Polynomial.map (algebraMap (Polynomial F) (RatFunc F)) ((bivariateCoefficientDerivative F) p) = Differential.mapCoeffs (Polynomial.map (algebraMap (Polynomial F) (RatFunc F)) p)

Mapping the inner coefficients of p into RatFunc F intertwines the inner derivative with coefficientwise rational differentiation.