English
For every k and d, the k-th iterated derivative of the cotTerm function with respect to z equals a rational expression: (-1)^k k! times the sum of two simple poles at z = -d-1 and z = d+1.
Русский
Для любых k и d производная по z от cotTerm z d, взятая k-й итерацией, равна сочетанию двух простых полюсов в точках z = -d-1 и z = d+1, умноженному на (-1)^k k!.
LaTeX
$$$$\forall k,d \in \mathbb{N},\\\;\;\; \text{EqOn}\left(\operatorname{iteratedDeriv} \\{k\}\; (\lambda z\;\cotTerm\, z\; d)\right) \\ (z \mapsto (-1)^k k! \left((z+(d+1))^{-1-k} + (z-(d+1))^{-1-k}\right)) \\ {\mathbb{C}_{\mathbb{Z}}}. $$$$
Lean4
theorem eqOn_iteratedDeriv_cotTerm (d : ℕ) :
EqOn (iteratedDeriv k (fun z ↦ cotTerm z d))
(fun z ↦ (-1) ^ k * k ! * ((z + (d + 1)) ^ (-1 - k : ℤ) + (z - (d + 1)) ^ (-1 - k : ℤ))) ℂ_ℤ :=
by
intro z hz
rw [← Pi.add_def, iteratedDeriv_add]
· have h2 := iter_deriv_inv_linear_sub k 1 ((d + 1 : ℂ))
have h3 := iter_deriv_inv_linear k 1 (d + 1 : ℂ)
simp only [one_div, one_mul, one_pow, mul_one, Int.reduceNeg, iteratedDeriv_eq_iterate] at *
rw [h2, h3]
ring
·
simpa [sub_eq_add_neg] using
(contDiffOn_inv_linear k (-(d + 1))).contDiffAt ((isOpen_compl_range_intCast).mem_nhds hz)
· simpa using (contDiffOn_inv_linear k (d + 1)).contDiffAt ((isOpen_compl_range_intCast).mem_nhds hz)
