summable_rpow_inv — Mathlib

English

For real p > 1, the p-series with reciprocal powers converges: ∑ 1/n^p converges.

Русский

Для действительного p > 1 p‑серия с обратной степенью сходится: ∑ 1/n^p сходится.

LaTeX

$$$$\displaystyle \sum_{n=1}^{\infty} \frac{1}{n^{p}} < \infty \quad\text{for } p>1.$$$$

Lean4

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

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