summable_one_div_nat_cpow — Mathlib

English

For complex p, the series ∑ 1/n^p converges iff Re(p) > 1.

Русский

Для комплексного p ряд ∑ 1/n^p сходится тогда и только тогда, когда Re(p) > 1.

LaTeX

$$$$\displaystyle \sum_{n=1}^{\infty} \frac{1}{n^{p}} \quad \text{converges } \iff \quad \operatorname{Re}(p) > 1.$$$$

Lean4

theorem summable_one_div_nat_cpow {p : ℂ} : Summable (fun n : ℕ ↦ 1 / (n : ℂ) ^ p) ↔ 1 < re p :=
  by
  rw [← Real.summable_one_div_nat_rpow, ← summable_nat_add_iff 1 (G := ℝ), ← summable_nat_add_iff 1 (G := ℂ), ←
    summable_norm_iff]
  simp only [norm_div, norm_one, ← ofReal_natCast, norm_cpow_eq_rpow_re_of_pos (Nat.cast_pos.mpr <| Nat.succ_pos _)]

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