English
For p a natural number, the series ∑_{n∈ℤ} 1/(n^p) converges if and only if 1 < p.
Русский
Для целого p > 1 серия ∑_{n∈ℤ} 1/(n^p) сходится тогда и только тогда, когда p > 1.
LaTeX
$$$$\displaystyle \sum_{n\in\mathbb{Z}} \frac{1}{n^{p}} \quad \text{converges } \iff \quad 1 < p.$$$$
Lean4
/-- Summability of the `p`-series over `ℤ`. -/
theorem summable_one_div_int_pow {p : ℕ} : (Summable fun n : ℤ ↦ 1 / (n : ℝ) ^ p) ↔ 1 < p :=
by
refine
⟨fun h ↦ summable_one_div_nat_pow.mp (h.comp_injective Nat.cast_injective), fun h ↦
.of_nat_of_neg (summable_one_div_nat_pow.mpr h)
(((summable_one_div_nat_pow.mpr h).mul_left <| 1 / (-1 : ℝ) ^ p).congr fun n ↦ ?_)⟩
rw [Int.cast_neg, Int.cast_natCast, neg_eq_neg_one_mul (n : ℝ), mul_pow, mul_one_div, div_div]
