Evaluating multivariate polynomials at dual numbers

Evaluating a polynomial p over R at the point of R[ε], ε² = 0, whose coordinate i is ε and whose other coordinates are 0 reads off two coefficients of p: its constant coefficient and its coefficient of the variable Xᵢ,

p(ε eᵢ) = p(0) + (coefficient of Xᵢ in p) ε.

As this evaluation is a ring homomorphism, it extracts the linear coefficient of Xᵢ from an element that is only known through a universal property, such as the image of an element of the Lazard ring in a polynomial ring.

More generally, evaluating p at v + ε w gives p(v) + ε ∑ⱼ wⱼ ∂ⱼp(v), so derivatives of polynomials can be computed as values over the dual numbers.

Main results

• MvPolynomial.aeval_single_eps: p(ε eᵢ) = p(0) + (coefficient of Xᵢ in p) ε.
• MvPolynomial.aeval_inl_add_inr: p(v + ε w) = p(v) + ε ∑ⱼ wⱼ ∂ⱼp(v).

theorem MvPolynomial.aeval_inl_add_inr {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Fintype σ] (f : MvPolynomial σ R) (v w : σ → R) : (aeval fun (j : σ) => TrivSqZeroExt.inl (v j) + TrivSqZeroExt.inr (w j)) f = TrivSqZeroExt.inl ((eval v) f) + TrivSqZeroExt.inr (∑ j : σ, w j * (eval v) ((pderiv j) f))

Evaluation at a dual-number point. Evaluating a polynomial at v + ε w, where ε² = 0, gives its value at v plus ε times its derivative at v in the direction w.

theorem MvPolynomial.aeval_single_eps {σ : Type u_1} {R : Type u_2} [CommSemiring R] [DecidableEq σ] (i : σ) (p : MvPolynomial σ R) : (aeval (Pi.single i DualNumber.eps)) p = (algebraMap R (DualNumber R)) (constantCoeff p) + p.coeff (Finsupp.single i 1) • DualNumber.eps

Evaluating p at the point ε eᵢ of the dual numbers gives p(0) + (coefficient of Xᵢ in p) ε.