Automatic proving some expression is positive Is there any automated (i.e., some algorithm) to prove that a certain algebraic expression is always non-negative in some range ? If so, is there any implementation you would suggest? My concrete problem is that I want to prove that for $f \in [0,1], 1 \leq a \leq L-2$ the following is true:
$$2^{(-a - L)} f^{-a} (1 + f)^{(-1 - a)} \left\{2^{(1 + a)} f^a (1 + f)^L (1 + 2 f) \left(-(1 + f)^{(1 + a)} + 2^a (1 + f^{(1 + a)})\right)\right.$$
$$ + 2^L (1 + f)^a \left[-2^a (1 + f) \left(-f^{(1 + 2 a)} + f^L + 3 f^{(a + L)} + 
3 f^{(1 + a + L)}\right) \right.$$
$$ \left.\left.+ (1 + f)^a \left((-3 + f) f^{(1 + a)} - a (-1 + f) (1 + 2 f) (f^a - f^L) + f^L (2 + 3 f (3 + f))\right)\right]\right\} >=0$$
 A: Some CASes do implement mechanisms that can sometimes answer such questions.  For example, in Maple you could specify the ranges of your parameters using assume() and then test for positivity using is() or coulditbe().  Mind you, it won't always work, and sometimes you might need to help the computer along.  In some ways, using a CAS like this effectively is just as much of an art as doing the math all by yourself.
In any case, you should start by simplifying your expression: the factor of $2^{-a-L} f^{-a} (1+f)^{-1-a}$ in the beginning, being a product of powers of non-negative numbers, is always non-negative and can therefore be omitted.  A decent CAS ought to figure that out for you, but there's no point in even bothering it with such things.
Also, this is a generic solving technique: if you can write your expression as a product, you can try to determine the sign of each factor separately.  Ditto if you have a sum and can show each term to be non-negative, although in that case even one bad term can spoil the whole sum.
More generally, try applying the intermediate value theorem.  In particular, if a function has no zeros and no discontinuities on an interval, and is positive for some value on that interval, it must be positive on all of it.  It's often easier, for both humans and computers, to just look for the zeros of a function than to directly deduce its sign.
A: You may want to look at global optimization methods. If you can compute a positive lower bound for the global minimum, then you're done.
