summable_nat_rpow — Mathlib

English

Let p be a real number. Then the series sum_{n=1}^∞ n^p converges if and only if p < −1.

Русский

Пусть p — действительное число. Тогда ряд ∑_{n=1}^∞ n^p сходится тогда и только тогда, когда p < −1.

LaTeX

$$$\displaystyle \sum_{n=1}^{\infty} n^{p} \quad \text{converges if and only if } p < -1.$$$

Lean4

@[simp]
theorem summable_nat_rpow {p : ℝ} : Summable (fun n => (n : ℝ) ^ p : ℕ → ℝ) ↔ p < -1 :=
  by
  rcases neg_surjective p with ⟨p, rfl⟩
  simp [rpow_neg]

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