summable_one_div_int_add_rpow — Mathlib

English

For real a and s, the series ∑_{n∈ℤ} 1/|n+a|^s converges if and only if s > 1.

Русский

Для вещественных a и s ряд ∑_{n∈ℤ} 1/|n+a|^s сходится тогда и только тогда, когда s > 1.

LaTeX

$$$$\displaystyle \sum_{n\in\mathbb{Z}} \frac{1}{|n+a|^{s}} < \infty \quad\text{iff}\quad s>1.$$$$

Lean4

theorem summable_one_div_int_add_rpow (a : ℝ) (s : ℝ) : Summable (fun n : ℤ ↦ 1 / |n + a| ^ s) ↔ 1 < s := by
  simp_rw [summable_int_iff_summable_nat_and_neg, ← abs_neg (↑(-_ : ℤ) + a), neg_add, Int.cast_neg, neg_neg,
    Int.cast_natCast, summable_one_div_nat_add_rpow, and_self]

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