summable_pow_mul_exp_neg_nat_mul — Mathlib

English

For any k ∈ ℕ and r > 0, the series ∑ n^k e^{-r n} converges.

Русский

Для любого k ∈ ℕ и r > 0 ряд ∑ n^k e^{-r n} сходится.

LaTeX

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

Lean4

theorem summable_pow_mul_exp_neg_nat_mul (k : ℕ) {r : ℝ} (hr : 0 < r) : Summable fun n : ℕ ↦ n ^ k * exp (-r * n) :=
  by
  simp_rw [mul_comm (-r), exp_nat_mul]
  apply summable_pow_mul_geometric_of_norm_lt_one
  rwa [norm_of_nonneg (exp_nonneg _), exp_lt_one_iff, neg_lt_zero]

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