English
The k-th derivative of the reciprocal function x ↦ x^{-1} is given by (-1)^k k! x^{-(1+k)}.
Русский
k-я производная функции обратной величины x^{-1} равна (-1)^k k! x^{-(1+k)}.
LaTeX
$$$\\mathrm{deriv}^[k] (x \\mapsto x^{-1}) = (-1)^k k! \\cdot x^{-(1+k)}$$$
Lean4
theorem iter_deriv_inv (k : ℕ) (x : 𝕜) : deriv^[k] Inv.inv x = (-1) ^ k * k ! * x ^ (-1 - k : ℤ) :=
calc
deriv^[k] Inv.inv x = deriv^[k] (· ^ (-1 : ℤ)) x := by simp
_ = (∏ i ∈ Finset.range k, (-1 - i : 𝕜)) * x ^ (-1 - k : ℤ) := (mod_cast iter_deriv_zpow (-1) x k)
_ = (-1) ^ k * k ! * x ^ (-1 - k : ℤ) :=
by
simp only [← neg_add', Finset.prod_neg, ← Finset.prod_Ico_id_eq_factorial, Finset.prod_Ico_eq_prod_range]
simp
