iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow

English

For hk ≥ 1 and z in the upper half-plane, iteratedDerivWithin k of π cot(π z) equals (-1)^k k! times the sum over ℤ of 1/(z+n)^{k+1}.

Русский

Для hk ≥ 1 и z в верхней полуплоскости, k-я итеративная производная π cot(π z) равна (-1)^k k! сумма по n∈ℤ от 1/(z+n)^{k+1}.

LaTeX

$$$$\forall k \ge 1,\; \forall z \in \mathbb{H}_0:\; \operatorname{iteratedDerivWithin} k\; (x \mapsto \pi \cot(\pi x))\; \mathbb{H}_0\, z = (-1)^k k! \; \sum_{n\in \mathbb{Z}} (z+n)^{-(k+1)}. $$$$

Lean4

/-- The series expansion of the iterated derivative of `π cot (π z)`. -/
theorem iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow {k : ℕ} (hk : 1 ≤ k) {z : ℂ} (hz : z ∈ ℍₒ) :
    iteratedDerivWithin k (fun x : ℂ ↦ π * cot (π * x)) ℍₒ z = (-1) ^ k * k ! * ∑' n : ℤ, 1 / (z + n) ^ (k + 1) :=
  by
  convert iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_zpow hk hz with n
  rw [show (-1 - k : ℤ) = -(k + 1 :) by norm_cast; cutsat, zpow_neg_coe_of_pos _ (by cutsat), one_div]

Похожие утверждения