iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_zpow

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 (z+n)^{−1−k}.

Русский

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

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)^{(-1-k)}. $$$$

Lean4

theorem iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_zpow {k : ℕ} (hk : 1 ≤ k) {z : ℂ} (hz : z ∈ ℍₒ) :
    iteratedDerivWithin k (fun x : ℂ ↦ π * cot (π * x)) ℍₒ z = (-1) ^ k * k ! * ∑' n : ℤ, (z + n) ^ (-1 - k : ℤ) :=
  by
  have h0 := iteratedDerivWithin_cot_pi_mul_sub_inv k hz
  rw [iteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum hk hz, add_comm] at h0
  rw [← add_left_inj (-(-1) ^ k * k ! * z ^ (-1 - k : ℤ)), h0]
  ring

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