Demostración automática de que una expresión es positiva

Question

¿Existe algún automatismo (es decir, algún algoritmo) para demostrar que una determinada expresión algebraica es siempre no negativa en algún intervalo? Si es así, ¿hay alguna implementación que me sugieras? Mi problema concreto es que quiero demostrar que para $f \in [0,1], 1 \leq a \leq L-2$ lo siguiente es cierto:

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

Algunos CAS aplican mecanismos que a veces pueden responder a estas preguntas. Por ejemplo, en Maple puede especificar los rangos de sus parámetros utilizando assume() y luego comprobar la positividad utilizando is() o coulditbe(). Eso sí, no siempre funcionará, y a veces tendrás que ayudar al ordenador. En cierto modo, utilizar un CAS como éste de forma eficaz es un arte tan grande como hacer los cálculos uno mismo.

En cualquier caso, debes empezar por simplificar tu expresión: el factor de $2^{-a-L} f^{-a} (1+f)^{-1-a}$ al principio, al ser un producto de potencias de números no negativos, siempre es no negativo y, por tanto, puede omitirse. Un CAS decente debería resolverlo por ti, pero no tiene sentido molestarlo con esas cosas.

Además, ésta es una técnica de resolución genérica: si puedes escribir tu expresión como un producto, puedes intentar determinar el signo de cada factor por separado. Lo mismo ocurre si tienes una suma y puedes demostrar que cada término no es negativo, aunque en ese caso incluso un término malo puede estropear toda la suma.

De forma más general, intenta aplicar el teorema del valor intermedio. En particular, si una función no tiene ceros ni discontinuidades en un intervalo, y es positiva para algún valor en ese intervalo, debe ser positiva en todo él. A menudo es más fácil, tanto para los humanos como para los ordenadores, buscar los ceros de una función que deducir directamente su signo.

Answer 2

Quizá le interese buscar métodos de optimización global. Si puedes calcular un límite inferior positivo para el mínimo global, ya está.

Answer 3

He aquí un posible enfoque, más ad hoc que los sugeridos anteriormente. Sea $E=E(f,L,a)$ ser la expresión sin el factor "manifiestamente positivo" que Willie Wong observó es irrelevante. Espero que establecer que para los números enteros $a$ llevará a resolverlo de verdad $a$ (es sólo una esperanza). Así que céntrate en la integralidad $a$ . Porque $a=1$ es un poco diferente, separar ese caso fuera. Así que ahora explorar $E(f,L,a)$ para $1 < a \le L-2$ donde ambos $a$ y $L$ son números enteros. Para $L$ incluso, $$E = -2^a \; f^{a+1} \; (1+f)^{a+1} \; \mathrm{poly}(f^{L+1}),$$ donde $\mathrm{poly}(f^{L+1})$ es un polinomio en $f$ de grado $L+1$ . Para $L$ impar, $$E = -2^a \; f^a \; (1+f)^{a+2} \; \mathrm{poly}(f^L).$$ Ejemplos, $L$ incluso: $$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$ impar: $$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).$$

Ahora la tarea es demostrar que $\mathrm{poly}(\;)$ es negativo para $f$ en $[0,1]$ . Como se ha observado anteriormente, $f=1$ es una raíz, por lo que $(f-1)$ es un factor. Tomando como ejemplo el último polinomio anterior, tiene una raíz en $f=-0.346213$ y es negativo entre allí y $f=1$ . Parece factible analizar la estructura de $\mathrm{poly}(\;)$ y demostrar que no tiene raíces en $[0,1]$ que lo resolvería para números enteros $a>1$ .

Por supuesto, soy consciente de que dejo mucho a la esperanza y al trabajo futuro.