Multivariate polynomials at dual numbers

Evaluating a multivariate polynomial at dual numbers computes its first-order Taylor expansion: the real part of P(z + ε v) is P(z) (MvPolynomial.fst_aeval_dualNumber) and its dual part is ∑_a ∂_a P(z) v_a (MvPolynomial.snd_aeval_dualNumber). This is the multivariate analogue of Polynomial.aeval_add_of_sq_eq_zero.

Main results

• MvPolynomial.fst_aeval_dualNumber: the real part of a polynomial at dual numbers.
• MvPolynomial.snd_aeval_dualNumber: Taylor expansion over the dual numbers.

theorem MvPolynomial.fst_aeval_dualNumber {σ : Type u_1} {R : Type u_2} [CommRing R] (P : MvPolynomial σ R) (u : σ → DualNumber R) : TrivSqZeroExt.fst ((aeval u) P) = (eval fun (a : σ) => TrivSqZeroExt.fst (u a)) P

The real part of a polynomial at dual numbers is its value at the real parts.

theorem MvPolynomial.snd_aeval_dualNumber {σ : Type u_1} {R : Type u_2} [CommRing R] [Fintype σ] (P : MvPolynomial σ R) (u : σ → DualNumber R) : TrivSqZeroExt.snd ((aeval u) P) = ∑ a : σ, (eval fun (b : σ) => TrivSqZeroExt.fst (u b)) ((pderiv a) P) * TrivSqZeroExt.snd (u a)

Taylor expansion over the dual numbers. The dual part of P(z + ε v) is ∑_a ∂_a P(z) v_a.