Automatic proving some expression is positive - MathOverflow

Automatic proving some expression is positive

2010-08-03T20:21:13Z

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

Answer by Ilmari Karonen for Automatic proving some expression is positive

2010-08-03T22:01:13Z

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.

Answer by lhf for Automatic proving some expression is positive

2010-08-04T02:28:38Z

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.

Answer by Joseph O'Rourke for Automatic proving some expression is positive

2010-08-04T13:09:07Z

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.