Help wanted: infinite sums over Z

Stream: maths

[David Loeffler]

I'm trying to get my Riemann-zeta-values project merged in the limited time window before the files it depends on get frozen for porting. This has come up in the review process and I'd be grateful for suggestions:

If f is a function ℤ → α for α a topological abelian group, and f has some (topological) sum a, then how can one show that has_sum (λ n:ℕ, f n + f (-n)) (a + f 0) without assuming any completeness or separation axioms on α? There is a proof of this in the library assuming that α is complete and Hausdorff (has_sum.sum_nat_of_sum_int), which I want to use in my new PR. The reviewer points out that these hypotheses should be removable, which seems plausible to me, but I don't see a simple way of proving it.

[Sebastien Gouezel]

I'll have a look.