# 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$$

-
What is the range on $L$? $L \in \mathbb{R}$ ? –  Joseph O'Rourke Aug 3 '10 at 21:00
Fixed up your math display for you. It looks like there is a lot more simplification that can be done for this expression. (For starters there is the manifestly positive multiplier outside the outermost curly brackets.) –  Willie Wong Aug 3 '10 at 21:14
This is of no help, but when $f=1$, the expression is zero. –  Joseph O'Rourke Aug 3 '10 at 21:15
L is an integer L >= 3. I plotted for some values of (a,L) and it looks like it is a function that is increasing up some point then decreasing back to zero (unimodal). Also: I have the feeling that it goes by some convexity argument. I've encountered similar expressions which I could prove it was positive by applying things of type (1+f^k)/2 >= ((1+f)/2)^k But since the expressions got larger for this application (this is a part of a Machine Learning problem) I don't know how to find the correct convexity arguments anymore. –  Renato Aug 3 '10 at 22:25
Either Joseph's comment, or Willie's correction of the original expression is wrong (now, when $f=1$, the last factor in the first line is $0$, the second line depends on $L$, and the third does not). Renato, please, reenter the original expression without erasing Willie's. –  fedja Aug 4 '10 at 3:18

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.

-

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.

-

Here is a possible approach, more ad hoc than those previously suggested. Let $E=E(f,L,a)$ be the expression without the "manifestly positive" factor that Willie Wong noticed is irrelevant. Hope that establishing it for integers $a$ will lead to settling it for real $a$ (that's just a hope). So focus on integral $a$. Because $a=1$ is a bit different, separate that case off. So now explore $E(f,L,a)$ for $1 < a \le L-2$, where both $a$ and $L$ are integers. For $L$ even, $$E = -2^a \; f^{a+1} \; (1+f)^{a+1} \; \mathrm{poly}(f^{L+1}),$$ where $\mathrm{poly}(f^{L+1})$ is a polynomial in $f$ of degree $L+1$. For $L$ odd, $$E = -2^a \; f^a \; (1+f)^{a+2} \; \mathrm{poly}(f^L).$$ Examples, $L$ even: $$L=6,a=2: \quad E = -8 f^2 (f+1)^3 \left(34 f^7-31 f^6-56 f^5+59 f^4+10 f^3+23 f^2-20 f-19\right).$$ $$L=6,a=3: \quad E = -16 f^3 (f+1)^4 \left(46 f^7-27 f^6-76 f^5+19 f^4+110 f^3-5 f^2-48 f-19\right).$$ $$L=6,a=4: \quad E = -32 f^4 (f+1)^5 \left(44 f^7-15 f^6-90 f^5+55 f^4+80 f^3+15 f^2-66 f-23\right).$$

$L$ odd: $$L=7,a=2: \quad E = -8 f^2 (f+1)^4 \left(74 f^7-127 f^6+91 f^4-46 f^3+39 f^2+4 f-35\right).$$

$$L=7,a=3: \quad E = -16 f^3 (f+1)^5 \left(106 f^7-147 f^6-36 f^5+55 f^4+74 f^3+27 f^2-48 f-31\right).$$

$$L=7,a=4: \quad E = -32 f^4 (f+1)^6 \left(118 f^7-143 f^6-56 f^5+15 f^4+174 f^3-f^2-76 f-31\right).$$

$$L=7,a=5: \quad E = -64 f^5 (f+1)^7 \left(104 f^7-105 f^6-106 f^5+137 f^4+28 f^3+73 f^2-90 f-41\right).$$

Now the task is prove that $\mathrm{poly}(\;)$ is negative for $f$ in $[0,1]$. As observed previously, $f=1$ is a root, so $(f-1)$ is a factor. Just taking the last polynomial above as an example, it has a root at $f=-0.346213$ and is negative between there and $f=1$. It seems feasible to analyze the structure of $\mathrm{poly}(\;)$ and prove that it has no roots in $[0,1]$, which would settle it for integers $a>1$.

Of course I am aware that I am leaving much to hope and further work.

-
Thanks. We are trying to investigate those polynomials. Actually, we are happy with $a,L \in \mathbb{Z}$ since this is enough for our application. The question somewhat reduces to proving that some polynomial has no roots in an interval. –  Renato Aug 4 '10 at 15:27
@Renato: Yes, I would say your question precisely reduces to showing that these polynomials have no root in [0,1]. Some of them have no real roots at all, e.g., for L=7, a=3,4, after factoring out (f-1). These may be easier to tackle first. –  Joseph O'Rourke Aug 5 '10 at 13:02