Prove a formula for a known convergent series with Resolve?

Questions
,
1

I ran across this behaviour that I do not understand. I wanted to prove a formula for a known convergent series:

\sum_{k=-\infty}^\infty \frac{1}{(2k+1)(2q-2k-1)} = -\frac{\pi^2}{4} \delta_{q,0}\quad for \quad q\in\mathbb{Z}.

However, Mathematica says this is wrong:

Resolve[ForAll[q, Sum[1/((2  k + 1) (2  q - 2  k - 1)) == -(\[Pi]^2/4)  KroneckerDelta[q, 0], {k,-Infinity,Infinity}], Integers]

returns False. Moreover, if the values for q are restricted, i.e. if I look separately at the cases q=0 and q\neq 0,
I get a True result: The two commands

Resolve[ForAll[q, q == 0, Sum[1/((2  k + 1) (2  q - 2  k - 1)) == -(\[Pi]^2/4)  KroneckerDelta[q, 0], {k,-Infinity,Infinity}], Integers]

Resolve[ForAll[q, q != 0, Sum[1/((2  k + 1) (2  q - 2  k - 1)) == -(\[Pi]^2/4)  KroneckerDelta[q, 0], {k,-Infinity,Infinity}], Integers]

both evaluate to True. Logically, this is a contradiction, so my question is whether I misunderstood the function of these commands or this is a bug.
Thanks in advance for clarification!
(Using Mathematica 10.0)

2

Hi Julian,

I guess the problem is that for the sum first the general case is evaluated, and this gives:

Sum[1/((2 k + 1) (2 q - 2 k - 1)), {k, -Infinity, Infinity}]
(*  Out:    -((\[Pi] Tan[\[Pi] q])/(4 q))   *)

So your first line reads:

Resolve[ForAll[q, -((\[Pi] Tan[\[Pi] q])/(4 q)) == -(\[Pi]^2/4) KroneckerDelta[q, 0]], Integers]

and this evaluates to False, because in the case q=0 we have:

(-((\[Pi] Tan[\[Pi] q])/(4 q)) == -(\[Pi]^2/4)) /. q -> 0
(*  Out:    Indeterminate\[Equal]-(\[Pi]^2/4)   *)

In this case you need the limit:

Limit[-((\[Pi] Tan[\[Pi] q])/(4 q)), q -> 0]

If you restrict the value of q before the sum gets evaluated (you second option above) everything works.

Hope that helps, regards ā€“ Henrik

3

Thanks for the insight!

This explains the result, but I am somewhat disappointed that the general case yields

-((\[Pi] Tan[\[Pi] q])/(4 q))

and not the continuous continuation of this expression.

Best regards, Julian