English
For hk ≥ 1 and z in the upper half-plane, the k-th iterated derivative of π cot(π z) − 1/z equals −(-1)^k k! z^{−1−k} plus (-1)^k k! ∑_{n∈ℤ} (z+n)^{−1−k}.
Русский
При hk ≥ 1 и z в верхней полуплоскости k-я итеративная производная функции π cot(π z) − 1/z равна −(-1)^k k! z^{−1−k} плюс (-1)^k k! ∑_{n∈ℤ} (z+n)^{−1−k}.
LaTeX
$$$$\forall k \ge 1,\; \forall z \in \mathbb{H}_0:\; \operatorname{iteratedDerivWithin} k\; (\lambda x. \pi \cot(\pi x) - 1/x)\; \mathbb{H}_0\, z \\= -(-1)^k \; k! \; z^{(-1-k)} + (-1)^k k! \; \sum_{n\in \mathbb{Z}} (z+n)^{(-1-k)}. $$$$
Lean4
theorem iteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum {k : ℕ} (hk : 1 ≤ k) (hz : z ∈ ℍₒ) :
iteratedDerivWithin k (fun x : ℂ ↦ π * cot (π * x) - 1 / x) ℍₒ z =
-(-1) ^ k * k ! * (z ^ (-1 - k : ℤ)) + (-1) ^ k * k ! * ∑' n : ℤ, (z + n) ^ (-1 - k : ℤ) :=
by
simp only [← aux_iteratedDeriv_tsum_cotTerm hk hz, one_div, neg_mul, neg_add_cancel_left]
refine iteratedDerivWithin_congr (fun z hz ↦ ?_) hz
simpa [cotTerm] using (cot_series_rep' (UpperHalfPlane.coe_mem_integerComplement ⟨z, hz⟩))
