Documentation

Mathlib.Analysis.PSeriesComplex

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