English
For a linear fractional function (c x + d)^{-1}, the k-th derivative is (-1)^k k! c^k (c x + d)^{-(1+k)}.
Русский
Для линейной дробноепеременной функции (c x + d)^{-1} k-я производная равна (-1)^k k! c^k (c x + d)^{-(1+k)}.
LaTeX
$$$\\mathrm{deriv}^[k] (x \\mapsto (c x + d)^{-1}) = (-1)^k k! \\cdot c^k \\cdot (c x + d)^{-(1+k)}$$$
Lean4
theorem iter_deriv_inv_linear (k : ℕ) (c d : 𝕜) :
deriv^[k] (fun x ↦ (c * x + d)⁻¹) = (fun x : 𝕜 ↦ (-1) ^ k * k ! * c ^ k * (c * x + d) ^ (-1 - k : ℤ)) := by
induction k with
| zero => simp
| succ k ihk =>
rw [factorial_succ, add_comm k 1, iterate_add_apply, ihk]
ext z
simp only [Int.reduceNeg, iterate_one, deriv_const_mul_field', cast_add, cast_one]
by_cases hd : c = 0
· simp [hd]
· have := deriv_comp_add_const (fun x ↦ (c * x) ^ (-1 - k : ℤ)) (d / c) z
have h0 : (fun x ↦ (c * (x + d / c)) ^ (-1 - (k : ℤ))) = (fun x ↦ (c * x + d) ^ (-1 - (k : ℤ))) :=
by
ext y
field_simp
rw [h0, deriv_comp_mul_left c (fun x ↦ (x) ^ (-1 - k : ℤ)) (z + d / c)] at this
simp [this]
field_simp
ring_nf
