Finiteness of zeta function

Stream: Is there code for X?

[Moritz Doll]

Do we have some version of $\sum_{k \in \mathbb{N}} (k + 1)^{-1-\varepsilon} < \infty$ for $\varepsilon > 0$? It shouldn't be too hard with docs#integrable_one_add_norm and the integral comparision theorems, but I did not find anything.

[Johan Commelin]

cc @David Loeffler ...

[David Loeffler]

Moritz Doll said:

Do we have some version of $\sum_{k \in \mathbb{N}} (k + 1)^{-1-\varepsilon} < \infty$ for $\varepsilon > 0$? It shouldn't be too hard with docs#integrable_one_add_norm and the integral comparision theorems, but I did not find anything.

Isn't this docs#real.summable_one_div_nat_rpow?

[Moritz Doll]

perfect, thank you