Convergence of p-series (complex case)

Here we show convergence of ∑ n : ℕ, 1 / n ^ p for complex p. This is done in a separate file rather than in Analysis.PSeries in order to keep the prerequisites of the former relatively light.

Tags

p-series, Cauchy condensation test

theorem Complex.summable_one_div_nat_cpow {p : ℂ} : (Summable fun (n : ℕ) => 1 / ↑n ^ p) ↔ 1 < p.re