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