summable_prod_mul_pow — Mathlib

English

The sum over pairs (a,b) of b^k · r^{a b} converges when |r|<1, via the sigma-antidiagonal encoding.

Русский

Сумма по парам (a,b) b^k · r^{a b} сходится при |r|<1 через кодирование антидиагонали.

LaTeX

$$$$ \sum_{(a,b) \in \mathbb{N}_+^2} b^{k} r^{a b} \text{ сходится при } |r|<1. $$$$

Lean4

theorem summable_prod_mul_pow (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) :
    Summable fun c : (ℕ+ × ℕ+) ↦ c.2 ^ k * (r ^ (c.1 * c.2 : ℕ)) := by
  simpa [sigmaAntidiagonalEquivProd.summable_iff.symm] using summable_divisorsAntidiagonal_aux k hr

Похожие утверждения