English
For every k ∈ ℕ and every r with ‖r‖ < 1, the generating series identity holds: ∑_{n≥1} n^k r^n/(1 − r^n) = ∑_{n≥1} σ_k(n) r^n.
Русский
Для любого k ∈ ℕ и любого r с ‖r‖ < 1 выполняется тождество генераторных рядов: ∑_{n≥1} n^k r^n/(1 − r^n) = ∑_{n≥1} σ_k(n) r^n.
LaTeX
$$$$\sum_{n=1}^{\infty} \frac{n^{k} r^{n}}{1 - r^{n}} = \sum_{n=1}^{\infty} \sigma_{k}(n) r^{n}, \quad \|r\|<1.$$$$
Lean4
theorem tsum_pow_div_one_sub_eq_tsum_sigma {r : 𝕜} (hr : ‖r‖ < 1) (k : ℕ) :
∑' n : ℕ+, n ^ k * r ^ (n : ℕ) / (1 - r ^ (n : ℕ)) = ∑' n : ℕ+, σ k n * r ^ (n : ℕ) :=
by
have (m : ℕ) [NeZero m] :=
tsum_geometric_of_norm_lt_one (ξ := r ^ m) (by simpa using pow_lt_one₀ (by simp) hr (NeZero.ne _))
simp only [div_eq_mul_inv, ← this, ← tsum_mul_left, mul_assoc, ← _root_.pow_succ',
← fun (n : ℕ) ↦ tsum_pnat_eq_tsum_succ (f := fun m ↦ n ^ k * (r ^ n) ^ m)]
have h00 := tsum_prod_pow_eq_tsum_sigma k hr
rw [Summable.tsum_comm (by apply (summable_prod_mul_pow k hr).prod_symm)] at h00
rw [← h00]
exact tsum_congr₂ <| fun b c ↦ by simp [mul_comm c.val b.val, pow_mul]
