English
A variant of the chain rule for aeval in a sum-decomposed polynomial, relating pderiv after aeval to pderiv after evaluating with a sum-elimination map.
Русский
Ограниченная формула цепной производной при суммировании разложения полинома: производная после aeval равна применению pderiv к исходному полиному через соответствующее отображение.
LaTeX
$$$$ \\text{aeval}(\\mathrm{Sum.elim}(X, C \\circ f))\\big( pderiv(\\mathrm{Sum.inl } j) p \\big) = pderiv j (\\text{aeval}(\\mathrm{Sum.elim}(X, C \\circ f)) p). $$$$
Lean4
theorem aeval_sumElim_pderiv_inl {S τ : Type*} [CommRing S] [Algebra R S] (p : MvPolynomial (σ ⊕ τ) R) (f : τ → S)
(j : σ) : aeval (Sum.elim X (C ∘ f)) ((pderiv (Sum.inl j)) p) = (pderiv j) ((aeval (Sum.elim X (C ∘ f))) p) := by
classical
induction p using MvPolynomial.induction_on with
| C a => simp
| add p q hp hq => simp [hp, hq]
| mul_X p q h =>
simp only [Derivation.leibniz, pderiv_X, smul_eq_mul, map_add, map_mul, aeval_X, h]
cases q <;> simp [Pi.single_apply]
