English
Extension of iterated derivative formula to natural indices: (deriv^[k] (x^n)) = (∏_{i=0}^{k-1} (n−i)) x^{n−k}.
Русский
Расширение формулы итеративной производной для натуральных индексов: (deriv^[k] (x^n)) = (∏_{i=0}^{k-1} (n−i)) x^{n−k}.
LaTeX
$$$\\; (\\mathrm{deriv}^[k] (x \\mapsto x^n))(x) = (\\prod_{i=0}^{k-1} (n - i)) \\cdot x^{n-k}$$$
Lean4
theorem iter_deriv_pow (n : ℕ) (x : 𝕜) (k : ℕ) :
deriv^[k] (fun x : 𝕜 => x ^ n) x = (∏ i ∈ Finset.range k, ((n : 𝕜) - i)) * x ^ (n - k) :=
by
simp only [← zpow_natCast, iter_deriv_zpow, Int.cast_natCast]
rcases le_or_gt k n with hkn | hnk
· rw [Int.ofNat_sub hkn]
· have : (∏ i ∈ Finset.range k, (n - i : 𝕜)) = 0 := Finset.prod_eq_zero (Finset.mem_range.2 hnk) (sub_self _)
simp only [this, zero_mul]
