summable_nat_pow_inv — Mathlib

English

For a natural exponent p, 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 1 < p.$$$

Lean4

/-- Test for convergence of the `p`-series: the real-valued series `∑' n : ℕ, (n ^ p)⁻¹` converges
if and only if `1 < p`. -/
@[simp]
theorem summable_nat_pow_inv {p : ℕ} : Summable (fun n => ((n : ℝ) ^ p)⁻¹ : ℕ → ℝ) ↔ 1 < p := by
  simp only [← rpow_natCast, summable_nat_rpow_inv, Nat.one_lt_cast]

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