English
A classical identity relating a Laurent-type series to a q-expansion: the n-th term of a certain cotangent-like series equals a constant times a q-series.
Русский
Классическое тождество между рядоподобной левой частью и q-разложением: коэффициенты ряда соответствуют q-ряду.
LaTeX
$$∑' n∈ℤ 1/(z+n)^{k+1} = ((-2πi)^{k+1}/k!) ∑' n∈ℕ n^k q^n, where q = e^{2πi z}.$$
Lean4
/-- This is one key identity relating infinite series to q-expansions 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 {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
have :
(-1) ^ k * k ! * ∑' n : ℤ, 1 / ((z : ℂ) + n) ^ (k + 1) =
-(2 * π * I) ^ (k + 1) * ∑' n : ℕ, n ^ k * cexp (2 * π * I * z) ^ n :=
by
rw [← iteratedDerivWithin_tsum_exp_aux_eq hk z, ←
iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow hk (by simpa using z.2)]
exact iteratedDerivWithin_congr (fun x hx ↦ by (simpa using pi_mul_cot_pi_q_exp ⟨x, hx⟩)) (by simpa using z.2)
simp_rw [(eq_inv_mul_iff_mul_eq₀ (by simp [Nat.factorial_ne_zero])).mpr this, ← tsum_mul_left]
congr
ext n
rw [show (-2 * π * I) ^ (k + 1) = (-1) ^ (k + 1) * (2 * π * I) ^ (k + 1) by rw [← neg_pow]; ring]
field_simp
ring_nf
simp [Nat.mul_two]
