MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).

2 fixed math display

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

$$2^{(-a - L) f^-a L)} f^{-a} (1 + f)^(-1 f)^{(-1 - a) (2^(1 a)} \left\{2^{(1 + a) a)} f^a (1 + f)^L (1 + 2 f) (-(1 \left(-(1 + f)^(1 f)^{(1 + a) a)} + 2^a (1 + f^(1 f^{(1 + a))) a)})\right)\right.$$ $$+ 2^L (1 + f)^a (-2^a \left[-2^a (1 + f) (-f^(1 \left(-f^{(1 + 2 a) a)} + f^L + 3 f^(a f^{(a + L) L)} + 3 f^(1 f^{(1 + a + L)L)}\right) + \right.$$ $$\left.\left.+ (1 + f)^a ((-3 \left((-3 + f) f^(1 f^{(1 + a) a)} - a (-1 + f) (1 + 2 f) (f^a - f^L) + f^L (2 + 3 f (3 + f))))) f))\right)\right]\right\} >=0=0$$

1

# 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) (2^(1 + a) f^a (1 + f)^L (1 + 2 f) (-(1 + f)^(1 + a) + 2^a (1 + f^(1 + a))) + 2^L (1 + f)^a (-2^a (1 + f) (-f^(1 + 2 a) + f^L + 3 f^(a + L) + 3 f^(1 + a + L)) + (1 + f)^a ((-3 + f) f^(1 + a) - a (-1 + f) (1 + 2 f) (f^a - f^L) + f^L (2 + 3 f (3 + f))))) >=0