summable_one_div_nat_rpow — Mathlib

English

Let p be a real number. The series ∑_{n=1}^∞ 1/n^p converges if and only if p > 1.

Русский

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

LaTeX

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

Lean4

/-- Test for convergence of the `p`-series: the real-valued series `∑' n : ℕ, 1 / n ^ p` converges
if and only if `1 < p`. -/
theorem summable_one_div_nat_rpow {p : ℝ} : Summable (fun n => 1 / (n : ℝ) ^ p : ℕ → ℝ) ↔ 1 < p := by simp

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