On the OEIS page for the double factorial, there are three ways of getting the sequence in PARI. One of them is this curious bit of PARI code:
a(n)=local(E); E=exp(x^2/2+x*O(x^n)); n!*polcoeff(1+E*x*(1+intformal(1/E)), n)
Compared to the others, the above may seem extraordinarily baroque:
a(n) = prod(i=0, floor((n-1)/2), n-2*i ); a(n)=if(n<2, 1, n*a(n-2))
In the example I'm asking about,
exp stands for the exponential function,
O for the zeroes of a p-adic or power series,
intformal for formal integration.
Is this a well-known use of the exponential function?
Is it known who first came up with this?
All of that seems like an amazing amount of mathematics to calculate the double factorial, and I'd like to know more about it.