English
A variant of the Eisenstein q-expansion identity for positive natural k, relating the cotangent-type sum to a series with n^k weights over natural numbers greater than zero.
Русский
Вариант тождества q-разложения Эйнштейна для положительного натурального k, связывающий ряд котангенса с ряд с весами n^k по натуральным числам > 0.
LaTeX
$$$(∑' n:ℤ) 1/(z+n)^{k+1} = ((-2πi)^{k+1}/k!) ∑' n:ℕ^+, n^k e^{2π i n z}$, при k≥1.$$
Lean4
/-- This is a version of `EisensteinSeries.qExpansion_identity` for positive naturals,
which shows that `∑' n, 1 / (z + n) ^ (k + 1) = ((-2 π I) ^ (k + 1) / k !) * ∑' n : ℕ+, n ^ k q ^n`
where `q = cexp (2 π I z)`. -/
theorem qExpansion_identity_pnat {k : ℕ} (hk : 1 ≤ k) (z : ℍ) :
∑' n : ℤ, 1 / ((z : ℂ) + n) ^ (k + 1) =
((-2 * π * I) ^ (k + 1) / k !) * ∑' n : ℕ+, n ^ k * cexp (2 * π * I * z) ^ (n : ℕ) :=
by
rw [EisensteinSeries.qExpansion_identity hk z, ← tsum_zero_pnat_eq_tsum_nat]
· simp [show k ≠ 0 by grind]
· apply (summable_pow_mul_cexp k 1 z).congr
simp
