The Coq mailing list

[Kevin Sullivan <sullivan.kevinj AT gmail.com>]

Right, it just relies on a non-standard definition of sum, see also Grandi series.

A colleague also wrote, :"One can also consider it as an example of analytic continuation. For example if z is not equal to 1 then 1/(1-z) = 1+z+z^2+.... The series on the right converges if |z|<1 with |z|=1 as a natural barrier.  Both sides agree (yield the same value) and are analytic if |z|<1. But the left side is exists and is analytic for all z not equal to 1. Therefore, the left side is the analytic continuation of the right side and hence can be used to assign a value to the infinite series on the right in regions where it does not converge." Mystery resolved.

On Tue, Feb 4, 2014 at 5:10 AM, Freek Wiedijk <freek AT cs.ru.nl> wrote:

Ramanujan summation