Automatic proving some expression is positive - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-25T08:27:14Z http://mathoverflow.net/feeds/question/34435 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/34435/automatic-proving-some-expression-is-positive Automatic proving some expression is positive Renato 2010-08-03T20:21:13Z 2010-08-04T13:23:38Z <p>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:</p> <p>$$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$$</p> http://mathoverflow.net/questions/34435/automatic-proving-some-expression-is-positive/34443#34443 Answer by Ilmari Karonen for Automatic proving some expression is positive Ilmari Karonen 2010-08-03T22:01:13Z 2010-08-03T22:01:13Z <p>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.</p> <p>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.</p> <p>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.</p> <p>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.</p> http://mathoverflow.net/questions/34435/automatic-proving-some-expression-is-positive/34468#34468 Answer by lhf for Automatic proving some expression is positive lhf 2010-08-04T02:28:38Z 2010-08-04T02:28:38Z <p>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.</p> http://mathoverflow.net/questions/34435/automatic-proving-some-expression-is-positive/34498#34498 Answer by Joseph O'Rourke for Automatic proving some expression is positive Joseph O'Rourke 2010-08-04T13:09:07Z 2010-08-04T13:23:38Z <p>Here is a possible approach, more <em>ad hoc</em> 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 &lt; 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).$$</p> <p>$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).$$</p> <p>$$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).$$</p> <p>$$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).$$</p> <p>$$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).$$</p> <p>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$.</p> <p>Of course I am aware that I am leaving much to hope and further work.</p>