English
If hp: p.map(algebraMap R A) = (X − C r)^q · p' holds, then aeval r (derivative^[q] p) = q! · p'.eval r.
Русский
Пусть hp: p.map(algebraMap R A) = (X − C r)^q · p' выполняется. Тогда aeval r (derivative^[q] p) = q! · p'.eval r.
LaTeX
$$$$ \text{If } p.map(\text{algebraMap } R A) = (X - C r)^q \cdot p' \text{ then } \mathrm{aeval}_r(\partial^q p) = q! \cdot p'.\mathrm{eval}_r. $$$$
Lean4
theorem aeval_iterate_derivative_self (p : R[X]) (q : ℕ) (r : A) {p' : A[X]}
(hp : p.map (algebraMap R A) = (X - C r) ^ q * p') : aeval r (derivative^[q] p) = q ! • p'.eval r :=
by
have h (x) (h : 1 ≤ x) (h' : x ≤ q) : (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1) :=
by
rw [← pow_add, add_tsub_cancel_of_le]
rwa [tsub_tsub_cancel_of_le h']
rw [aeval_def, eval₂_eq_eval_map, ← iterate_derivative_map]
simp_rw [hp, iterate_derivative_mul, iterate_derivative_X_sub_pow, ← smul_mul_assoc, smul_smul]
rw [sum_range_succ', Nat.choose_zero_right, one_mul, tsub_zero, Nat.descFactorial_self, tsub_self, pow_zero,
smul_mul_assoc, one_mul, Function.iterate_zero_apply, eval_add, eval_smul]
convert zero_add _
rw [eval_finset_sum]
apply sum_eq_zero
intro x hx
rw [h (x + 1) le_add_self (Nat.add_one_le_iff.mpr (mem_range.mp hx)), pow_one, eval_mul, eval_smul, eval_mul,
eval_sub, eval_X, eval_C, sub_self, zero_mul, smul_zero, zero_mul]
