My colleagues and I are working on a project related to an old paper of C. Borell and we have boiled it down to the following problem:
Show, for all integers $1 \leq i \leq k$, that the univariate real polynomial $P(x) = \frac12 \binom{2k}{2i} (1+x)^{2k-2i} + \frac12 Q(x)$ is everywhere nonnegative, where $Q(x) = \sum_{j=i}^k \binom{2k}{2j}(1-x)^{2k-2j}\binom{j}{i}(-4x)^{j-i}$.
(For what it's worth, Maple recognizes $Q(x)$ as $\binom{2k}{2i} (1-x)^{2k-2i} \text{hypergeom}([-(k-i), -(k-i)+\frac12], [i+\frac12], -4x/(1-x)^2)$.
I'm not asking MO to prove this (although I suppose if someone saw how to do so immediately I wouldn't turn down the answer). Instead, I'm asking "Is this 'routine'?" in the sense of the word used in the Petkovsek-Wilf-Zeilberger A=B book? In other words, would Doron Zeilberger say, "Oh yes, just type the following into Maple and it will produce a proof of the claim"? In other other words, does this question fall into a class of problems known to be decidable?
Of course, for any fixed $i$ and $k$ the problem is 'routine'. E.g., for $k = 4$, $i = 2$, we have $P(x) = 70x^4-168x^3+804x^2-168x+70$ and furthermore I can coax my computer into proving that's nonnegative. (Say, by obtaining a sum-of-squares representation like $P(x) = 42(x-1)^4 + 28x^4 + 552x^2+28$.)
I don't know the "A=B technology" very well: my question is whether it, or any other techniques, can be used to automatically prove these inequalities. I would also be happy to accept an answer explaining why proving these inequalities is not obviously 'routine' and will require some ingenuity.
UPDATE: Doron Zeilberger wrote me an email describing why at least 'half' of this problem is routine: namely, that for $i$ symbolic and $k-i$ numeric the nonnegativity can be proven by computer. He preferred not to post himself but said I could post his ideas here; I will do so once I get a chance to think about them.