My colleagues and I are working on a project related to an [old paper of C. Borell](http://www.springerlink.com/content/bp92875n35324173/) 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.



Proving univariate polynomials (defined by sums, binomial coeffs, etc.) are nonnegative: is it 'routine'?
There are some techniques for proving positivity of sums using computer
algebra, but they are all heuristic approaches rather than solid algorithms.
This is in contrast to identities, which we understand very well
algorithmically.


One possibility to prove positivity of some quantity f[n] involving a
discrete parameter n is to search for a "witness recurrence", for instance
of the form


f[n+2] == a[n] f[n+1] + b[n] f[n]


where a[n] and b[n] are positive rational functions. Once such a recurrence
is found, positivity of f[n] follows easily by induction.


Such a witness recurrence need not exist, but if it does, it is typically
routine to find (and prove!) it with computer algebra.


For your particular family of polynomials, I found the following recurrence,
which implies positivity for a decent portion of indices (k,i), albeit not
for all:


(1 + i)\*(7 + 6\*i + 13\*k)\*f[k, i]
= - (1 + i - 2\*k)\*(7 + 6\*i - k)*f[k-2, i-2]
 + 2*(7+13\*i+6\*i^2-20\*k-13\*i\*k+13\*k^2)\*(1+x)^2\*f[k-2, i-1]
 - (1 + i)\*(7 + 6\*i - 13\*k)\*(1 + x)^4\*f[k-2, i]
 - 2\*(-7 + 8\*i + 6\*i^2 - 20\*k - 13\*k^2)*f[k-1, i-1]
 + 4*(1 + i)\*(10 + 3\*i)\*(1 + x)^2\*f[k-1, i]


Observe that the polynomial coefficients of this recurrence are nonnegative
whenever 1<=i<=k, EXCEPT the coefficient in front of f[k-2,i-2], which
becomes negative for 6i+7 < k. So this recurrences suffices to prove
positivity for all i,k with 1<=i<=k<=7+6i.


(You may not see with with the naked eye that the nonlinear polynomials in
front of f[k-2,i-1] and f[k-1,i-1] are indeed positive for all i,k with
1<=i<=k, but confirming this is routine for the computer, e.g., using
Collins's algorithm for Cylindrical Algebraic Decomposition.)


There are some other recurrences of similar shape, only slightly more
complicated, for which the portion of indices (i,k) not covered is smaller.
But I was not able to find a recurrence that proves positivity for all i,k
in question. Maybe it's possible with some effort.


Following Doron's observation that g[L] := f[i,L+i] is a polynomial in x and
i for every fixed L, there is a linear recurrence of order 3 for g[L] with
polynomial coefficients in L,i,x, which implies positivity under certain
(ugly) restrictions on i and x but not in full generality.


For a fixed positive integer L, you can show positivity of g[L] in
Mathematica most easily as follows. Define the function


check[L\_Integer] := CylindricalDecomposition[Implies[i>=1,
Factor[FunctionExpand[1/2 Binomial2(i+L),2i^(2(i+L)-2i) + 1/2
Sum[Binomial2(i+L),2j^(2(i+L)-2j)Binomialj,i^(j-i),{j,i,(i+L)}]]/Pochhammer[i+1,L]] >= 0], {x,i}]


then check[10] evaluates to True in about 20sec (on my computer), proving
the positivity for L=10.


