summable_rpow — Mathlib

English

Let p be a real number. The series ∑ (n^p) converges iff p < −1.

Русский

Пусть p — действительное число. Ряд ∑ (n^p) сходится тогда и только тогда, когда p < −1.

LaTeX

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

Lean4

@[simp]
theorem summable_rpow {p : ℝ} : Summable (fun n => (n : ℝ≥0) ^ p : ℕ → ℝ≥0) ↔ p < -1 := by simp [← NNReal.summable_coe]

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