English
For any natural k, the k-th ordinary derivative D^k on polynomials satisfies D^k = k! · HasDeriv_k. Equivalently, k! times the k-th Hasse derivative equals the k-th iterate of the standard derivative.
Русский
Для любого натурального k обычная производная D^k на полиномах удовлетворяет D^k = k! · HasDeriv_k. Иными словами, k! умножает k‑ю Хассе-деривативу, получая k‑ю повторную производную.
LaTeX
$$$$ k! \cdot \mathrm{hasseDeriv}_k = (\mathrm{derivative})^{k} $$$$
Lean4
theorem factorial_smul_hasseDeriv : ⇑(k ! • @hasseDeriv R _ k) = (@derivative R _)^[k] :=
by
induction k with
| zero => rw [hasseDeriv_zero, factorial_zero, iterate_zero, one_smul, LinearMap.id_coe]
| succ k ih => ?_
ext f n : 2
rw [iterate_succ_apply', ← ih]
simp only [LinearMap.smul_apply, coeff_smul, LinearMap.map_smul_of_tower, coeff_derivative, hasseDeriv_coeff,
← @choose_symm_add _ k]
simp only [nsmul_eq_mul, factorial_succ, mul_assoc, succ_eq_add_one, ← add_assoc, add_right_comm n 1 k, ← cast_succ]
rw [← (cast_commute (n + 1) (f.coeff (n + k + 1))).eq]
simp only [← mul_assoc]
norm_cast
congr 2
rw [mul_comm (k + 1) _, mul_assoc, mul_assoc]
congr 1
have : n + k + 1 = n + (k + 1) := by apply add_assoc
rw [← choose_symm_of_eq_add this, choose_succ_right_eq, mul_comm]
congr
rw [add_assoc, add_tsub_cancel_left]
