summable_abs_int_rpow — Mathlib

English

If b > 1, then the series ∑_{n∈ℤ} |n|^{−b} converges.

Русский

Если b > 1, то серия по целым числам \sum_{n∈ℤ} |n|^{−b} сходится.

LaTeX

$$$$\displaystyle \sum_{n\in\mathbb{Z}} |n|^{-b} < \infty \quad\text{for } b>1.$$$$

Lean4

theorem summable_abs_int_rpow {b : ℝ} (hb : 1 < b) : Summable fun n : ℤ => |(n : ℝ)| ^ (-b) :=
  by
  apply Summable.of_nat_of_neg
  on_goal 2 => simp_rw [Int.cast_neg, abs_neg]
  all_goals
    simp_rw [Int.cast_natCast, fun n : ℕ => abs_of_nonneg (n.cast_nonneg : 0 ≤ (n : ℝ))]
    rwa [summable_nat_rpow, neg_lt_neg_iff]

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