English
There is a classical identity relating a cotangent-type sum to a q-expansion: the sum over integers of 1/(z+n)^(k+1) equals ((-2π i)^(k+1)/k!) times the q-expansion sum ∑ n^k q^n with q = exp(2π i z), valid for k ≥ 1.
Русский
Существует классическое тождество, связывающее суммa типа cotangent с q-разложением: сумма по целым числам 1/(z+n)^(k+1) равна ((-2π i)^(k+1)/k!) умножить на q-разложение ∑ n^k q^n, где q = exp(2π i z), при k ≥ 1.
LaTeX
$$$\sum_{n∈\mathbb{Z}} \dfrac{1}{(z+n)^{k+1}} = \dfrac{(-2\pi i)^{k+1}}{k!} \sum_{n∈\mathbb{N}} n^k \mathrm{e}^{2\pi i z n}.$$$
Lean4
theorem iteratedDerivWithin_tsum_cexp_eq (k : ℕ) (z : ℍ) :
iteratedDerivWithin k (fun z ↦ ∑' n : ℕ, cexp (2 * π * I * z) ^ n) ℍₒ z =
∑' n : ℕ, iteratedDerivWithin k (fun s : ℂ ↦ cexp (2 * π * I * s) ^ n) ℍₒ z :=
by
rw [iteratedDerivWithin_tsum k isOpen_upperHalfPlaneSet (by simpa using z.2)]
· exact fun x hx ↦ summable_geometric_iff_norm_lt_one.mpr (UpperHalfPlane.norm_exp_two_pi_I_lt_one ⟨x, hx⟩)
· exact fun n _ _ ↦ summableLocallyUniformlyOn_iteratedDerivWithin_cexp n
· exact fun n l z hl hz ↦ differentiableAt_iteratedDerivWithin_cexp n l isOpen_upperHalfPlaneSet hz
