summable_exp_neg_nat — Mathlib

English

The series ∑ exp(n a) converges for a < 0; more generally, ∑ n^k exp(-r n) converges for r > 0.

Русский

Суммируемость ряда \sum n^k e^{-r n} при r > 0; и в частном случае ∑ e^{n a} сходится при a < 0.

LaTeX

$$$\sum_{n=0}^{\infty} n^{k} e^{-r n} \quad \text{converges if } r > 0$$$

Lean4

theorem summable_exp_neg_nat : Summable fun n : ℕ ↦ exp (-n) := by
  simpa only [mul_neg_one] using summable_exp_nat_mul_iff.mpr neg_one_lt_zero

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