summable_one_div_nat_pow — Mathlib

English

For p a natural number, the series ∑_{n=1}^∞ 1/(n^p) converges if and only if 1 < p.

Русский

Для целого числа p > 1 ряд ∑_{n=1}^∞ 1/(n^p) сходится тогда и только тогда, когда p > 1.

LaTeX

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

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_pow {p : ℕ} : Summable (fun n => 1 / (n : ℝ) ^ p : ℕ → ℝ) ↔ 1 < p := by
  simp only [one_div, Real.summable_nat_pow_inv]

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