summable_exp_nat_mul_iff — Mathlib

English

For any real a, the series ∑ exp(n a) converges if and only if a < 0.

Русский

Для любого вещественного a ряд \sum_{n≥0} e^{n a} сходится тогда и только тогда, когда a < 0.

LaTeX

$$$\sum_{n=0}^{\infty} e^{n a} \text{ is convergent } \iff a < 0$$$

Lean4

theorem summable_exp_nat_mul_iff {a : ℝ} : Summable (fun n : ℕ ↦ exp (n * a)) ↔ a < 0 := by
  simp only [exp_nat_mul, summable_geometric_iff_norm_lt_one, norm_of_nonneg (exp_nonneg _), exp_lt_one_iff]

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