English
Let k ∈ ℕ and r ∈ 𝕜 with ‖r‖ < 1. Then the double series over positive integers d and c satisfies the identity
∑_{d≥1} ∑_{c≥1} c^k r^{d c} = ∑_{e≥1} σ_k(e) r^e.
Русский
Пусть k ∈ ℕ и r ∈ 𝕜 удовлетворяют ‖r‖ < 1. Тогда двойной ряд по положительным d, c выполняет тождество
∑_{d≥1} ∑_{c≥1} c^k r^{d c} = ∑_{e≥1} σ_k(e) r^e.
LaTeX
$$$$\sum_{d=1}^{\infty} \sum_{c=1}^{\infty} c^{k} r^{d c} = \sum_{e=1}^{\infty} \sigma_{k}(e) r^{e}, \quad \|r\|<1.$$$$
Lean4
theorem tsum_prod_pow_eq_tsum_sigma (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) :
∑' d : ℕ+, ∑' c : ℕ+, c ^ k * r ^ (d * c : ℕ) = ∑' e : ℕ+, σ k e * r ^ (e : ℕ) :=
by
suffices ∑' c : ℕ+ × ℕ+, c.2 ^ k * r ^ (c.1 * c.2 : ℕ) = ∑' e : ℕ+, σ k e * r ^ (e : ℕ) by
rwa [← (summable_prod_mul_pow k hr).tsum_prod]
simp only [← sigmaAntidiagonalEquivProd.tsum_eq, sigmaAntidiagonalEquivProd, divisorsAntidiagonalFactors, PNat.mk_coe,
Equiv.coe_fn_mk, sigma_eq_sum_div, cast_sum, cast_pow, Summable.tsum_sigma (summable_divisorsAntidiagonal_aux k hr)]
refine tsum_congr fun n ↦ ?_
simpa [tsum_fintype, Finset.sum_mul,
(n : ℕ).divisorsAntidiagonal.sum_attach fun x : ℕ × ℕ ↦ x.2 ^ k * r ^ (x.1 * x.2),
sum_divisorsAntidiagonal fun x y ↦ y ^ k * r ^ (x * y)] using
Finset.sum_congr rfl fun i hi ↦ by rw [Nat.mul_div_cancel' (dvd_of_mem_divisors hi)]
