added description of two functions

examples.ipynb

@@ -759,10 +759,10 @@
       "From weighted AM-GM inequality:\n",
       "$$2a^2b^2c^3d \\le a^3bc^2d^2+ab^3c^4$$\n",
       "$$2a^2c^3d \\le a^3c^2d^2+ac^4$$\n",
-      "$$4a^2bc^3d \\le a^3bc^2d^2+a^3c^2d^2+ab^3c^4+ac^4$$\n",
+      "$$4a^2bc^3d \\le a^3bc^2d^2+a^3c^2d^2+ab^2c^4+abc^4$$\n",
       "\n",
       "$$  0  \\le \n",
-      "4a^3bcd^3+2a^3bd^4+2a^3cd^3+2a^2b^2cd^3+4a^2bc^2d^2+12a^2bcd^3+6a^2bd^4+4a^2c^2d^2+6a^2cd^3+4ab^3c^3d+2ab^3c^2d^2+6ab^2c^4+8ab^2c^3d+4ab^2c^2d^2+4ab^2cd^3+6abc^4+4abc^3d+6abc^2d^2+12abcd^3+6abd^4+4ac^2d^2+6acd^3+2b^3c^3d+2b^3c^2d^2+4b^2c^3d+4b^2c^2d^2+2b^2cd^3+2bc^3d+4bc^2d^2+4bcd^3+2bd^4+2c^2d^2+2cd^3  $$\n",
+      "4a^3bcd^3+2a^3bd^4+2a^3cd^3+2a^2b^2cd^3+4a^2bc^2d^2+12a^2bcd^3+6a^2bd^4+4a^2c^2d^2+6a^2cd^3+ab^3c^4+4ab^3c^3d+2ab^3c^2d^2+5ab^2c^4+8ab^2c^3d+4ab^2c^2d^2+4ab^2cd^3+5abc^4+4abc^3d+6abc^2d^2+12abcd^3+6abd^4+ac^4+4ac^2d^2+6acd^3+2b^3c^3d+2b^3c^2d^2+4b^2c^3d+4b^2c^2d^2+2b^2cd^3+2bc^3d+4bc^2d^2+4bcd^3+2bd^4+2c^2d^2+2cd^3  $$\n",
       "The sum of all inequalities gives us a proof of the inequality.\n"
      ]
     },
@@ -781,6 +781,214 @@
     "prove(makesubs(formula,'[0,c],[0,d]')*2)"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Function `powerprove` is a shortcut for splitting domain $R_+^n$ on several subdomains and proving the inequality for each of them. This function uses $2^n$ of $n$-dimensional intervals with a common point (by default it's $(1,1,...,1)$), where $n$ is a number of variables. Here there are two examples of using it. As you can see, proofs are very long."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 20,
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "numerator: $$x^4-4x^3+6x^2-4x+1$$\n",
+      "denominator: $$1$$\n",
+      "\n",
+      "\\hline\n",
+      "\n",
+      "Substitute $x\\to 1+x$\n",
+      "Numerator after substitutions: x^4\n",
+      "status: 0\n",
+      "\n",
+      "$$  0  \\le \n",
+      "x^4  $$\n",
+      "The sum of all inequalities gives us a proof of the inequality.\n",
+      "\n",
+      "\\hline\n",
+      "\n",
+      "Substitute $x\\to 1/(1+x)$\n",
+      "Numerator after substitutions: x^4\n",
+      "status: 0\n",
+      "\n",
+      "$$  0  \\le \n",
+      "x^4  $$\n",
+      "The sum of all inequalities gives us a proof of the inequality.\n"
+     ]
+    }
+   ],
+   "source": [
+    "powerprove('(x-1)^4')"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 19,
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "numerator: $$4a^5+4a^4b+4a^4c-6a^4-4a^3b-2a^3c+4ab^3-9ab^2+4ac^2-18ac+9a+4b^4+4b^3c-6b^3-3b^2c+4bc^2-12bc+10b+4c^3-6c^2+11c$$\n",
+      "denominator: $$1$$\n",
+      "\n",
+      "\\hline\n",
+      "\n",
+      "Substitute $a\\to 1+a,b\\to 1+b,c\\to 1+c$\n",
+      "Numerator after substitutions: 4a^5+4a^4b+4a^4c+22a^4+12a^3b+14a^3c+42a^3+12a^2b+18a^2c+34a^2+4ab^3+3ab^2-2ab+4ac^2+4b^4+4b^3c+18b^3+9b^2c+18b^2+4bc^2+2bc+4c^3+14c^2\n",
+      "status: 0\n",
+      "From weighted AM-GM inequality:\n",
+      "$$2ab \\le a^2+b^2$$\n",
+      "\n",
+      "$$  0  \\le \n",
+      "4a^5+4a^4b+4a^4c+22a^4+12a^3b+14a^3c+42a^3+12a^2b+18a^2c+33a^2+4ab^3+3ab^2+4ac^2+4b^4+4b^3c+18b^3+9b^2c+17b^2+4bc^2+2bc+4c^3+14c^2  $$\n",
+      "The sum of all inequalities gives us a proof of the inequality.\n",
+      "\n",
+      "\\hline\n",
+      "\n",
+      "Substitute $a\\to 1/(1+a),b\\to 1+b,c\\to 1+c$\n",
+      "Numerator after substitutions: 4a^5b^4+4a^5b^3c+14a^5b^3+9a^5b^2c+15a^5b^2+4a^5bc^2+2a^5bc+6a^5b+4a^5c^3+10a^5c^2+8a^5c+10a^5+20a^4b^4+20a^4b^3c+74a^4b^3+45a^4b^2c+78a^4b^2+20a^4bc^2+10a^4bc+24a^4b+20a^4c^3+54a^4c^2+30a^4c+40a^4+40a^3b^4+40a^3b^3c+156a^3b^3+90a^3b^2c+162a^3b^2+40a^3bc^2+20a^3bc+36a^3b+40a^3c^3+116a^3c^2+40a^3c+60a^3+40a^2b^4+40a^2b^3c+164a^2b^3+90a^2b^2c+168a^2b^2+40a^2bc^2+20a^2bc+20a^2b+40a^2c^3+124a^2c^2+18a^2c+34a^2+20ab^4+20ab^3c+86ab^3+45ab^2c+87ab^2+20abc^2+10abc+2ab+20ac^3+66ac^2+4b^4+4b^3c+18b^3+9b^2c+18b^2+4bc^2+2bc+4c^3+14c^2\n",
+      "status: 0\n",
+      "\n",
+      "$$  0  \\le \n",
+      "4a^5b^4+4a^5b^3c+14a^5b^3+9a^5b^2c+15a^5b^2+4a^5bc^2+2a^5bc+6a^5b+4a^5c^3+10a^5c^2+8a^5c+10a^5+20a^4b^4+20a^4b^3c+74a^4b^3+45a^4b^2c+78a^4b^2+20a^4bc^2+10a^4bc+24a^4b+20a^4c^3+54a^4c^2+30a^4c+40a^4+40a^3b^4+40a^3b^3c+156a^3b^3+90a^3b^2c+162a^3b^2+40a^3bc^2+20a^3bc+36a^3b+40a^3c^3+116a^3c^2+40a^3c+60a^3+40a^2b^4+40a^2b^3c+164a^2b^3+90a^2b^2c+168a^2b^2+40a^2bc^2+20a^2bc+20a^2b+40a^2c^3+124a^2c^2+18a^2c+34a^2+20ab^4+20ab^3c+86ab^3+45ab^2c+87ab^2+20abc^2+10abc+2ab+20ac^3+66ac^2+4b^4+4b^3c+18b^3+9b^2c+18b^2+4bc^2+2bc+4c^3+14c^2  $$\n",
+      "The sum of all inequalities gives us a proof of the inequality.\n",
+      "\n",
+      "\\hline\n",
+      "\n",
+      "Substitute $a\\to 1+a,b\\to 1/(1+b),c\\to 1+c$\n",
+      "Numerator after substitutions: 4a^5b^4+16a^5b^3+24a^5b^2+16a^5b+4a^5+4a^4b^4c+18a^4b^4+16a^4b^3c+76a^4b^3+24a^4b^2c+120a^4b^2+16a^4bc+84a^4b+4a^4c+22a^4+14a^3b^4c+30a^3b^4+56a^3b^3c+132a^3b^3+84a^3b^2c+216a^3b^2+56a^3bc+156a^3b+14a^3c+42a^3+18a^2b^4c+22a^2b^4+72a^2b^3c+100a^2b^3+108a^2b^2c+168a^2b^2+72a^2bc+124a^2b+18a^2c+34a^2+4ab^4c^2+ab^4+16ab^3c^2+8ab^3+24ab^2c^2+9ab^2+16abc^2+2ab+4ac^2+4b^4c^3+10b^4c^2+3b^4c+4b^4+16b^3c^3+44b^3c^2+8b^3c+18b^3+24b^2c^3+72b^2c^2+3b^2c+18b^2+16bc^3+52bc^2-2bc+4c^3+14c^2\n",
+      "status: 0\n",
+      "From weighted AM-GM inequality:\n",
+      "$$2bc \\le b^2+c^2$$\n",
+      "\n",
+      "$$  0  \\le \n",
+      "4a^5b^4+16a^5b^3+24a^5b^2+16a^5b+4a^5+4a^4b^4c+18a^4b^4+16a^4b^3c+76a^4b^3+24a^4b^2c+120a^4b^2+16a^4bc+84a^4b+4a^4c+22a^4+14a^3b^4c+30a^3b^4+56a^3b^3c+132a^3b^3+84a^3b^2c+216a^3b^2+56a^3bc+156a^3b+14a^3c+42a^3+18a^2b^4c+22a^2b^4+72a^2b^3c+100a^2b^3+108a^2b^2c+168a^2b^2+72a^2bc+124a^2b+18a^2c+34a^2+4ab^4c^2+ab^4+16ab^3c^2+8ab^3+24ab^2c^2+9ab^2+16abc^2+2ab+4ac^2+4b^4c^3+10b^4c^2+3b^4c+4b^4+16b^3c^3+44b^3c^2+8b^3c+18b^3+24b^2c^3+72b^2c^2+3b^2c+17b^2+16bc^3+52bc^2+4c^3+13c^2  $$\n",
+      "The sum of all inequalities gives us a proof of the inequality.\n",
+      "\n",
+      "\\hline\n",
+      "\n",
+      "Substitute $a\\to 1/(1+a),b\\to 1/(1+b),c\\to 1+c$\n",
+      "Numerator after substitutions: 4a^5b^4c^3+6a^5b^4c^2+11a^5b^4c+9a^5b^4+16a^5b^3c^3+28a^5b^3c^2+40a^5b^3c+38a^5b^3+24a^5b^2c^3+48a^5b^2c^2+51a^5b^2c+57a^5b^2+16a^5bc^3+36a^5bc^2+30a^5bc+34a^5b+4a^5c^3+10a^5c^2+8a^5c+10a^5+20a^4b^4c^3+34a^4b^4c^2+45a^4b^4c+40a^4b^4+80a^4b^3c^3+156a^4b^3c^2+160a^4b^3c+170a^4b^3+120a^4b^2c^3+264a^4b^2c^2+195a^4b^2c+246a^4b^2+80a^4bc^3+196a^4bc^2+110a^4bc+136a^4b+20a^4c^3+54a^4c^2+30a^4c+40a^4+40a^3b^4c^3+76a^3b^4c^2+70a^3b^4c+70a^3b^4+160a^3b^3c^3+344a^3b^3c^2+240a^3b^3c+300a^3b^3+240a^3b^2c^3+576a^3b^2c^2+270a^3b^2c+414a^3b^2+160a^3bc^3+424a^3bc^2+140a^3bc+204a^3b+40a^3c^3+116a^3c^2+40a^3c+60a^3+40a^2b^4c^3+84a^2b^4c^2+48a^2b^4c+58a^2b^4+160a^2b^3c^3+376a^2b^3c^2+152a^2b^3c+248a^2b^3+240a^2b^2c^3+624a^2b^2c^2+138a^2b^2c+312a^2b^2+160a^2bc^3+456a^2bc^2+52a^2bc+116a^2b+40a^2c^3+124a^2c^2+18a^2c+34a^2+20ab^4c^3+46ab^4c^2+15ab^4c+19ab^4+80ab^3c^3+204ab^3c^2+40ab^3c+82ab^3+120ab^2c^3+336ab^2c^2+15ab^2c+81ab^2+80abc^3+244abc^2-10abc-2ab+20ac^3+66ac^2+4b^4c^3+10b^4c^2+3b^4c+4b^4+16b^3c^3+44b^3c^2+8b^3c+18b^3+24b^2c^3+72b^2c^2+3b^2c+18b^2+16bc^3+52bc^2-2bc+4c^3+14c^2\n",
+      "status: 0\n",
+      "From weighted AM-GM inequality:\n",
+      "$$2ab \\le a^2+b^2$$\n",
+      "$$2bc \\le b^2+c^2$$\n",
+      "$$10abc \\le 5a^2b+5bc^2$$\n",
+      "\n",
+      "$$  0  \\le \n",
+      "4a^5b^4c^3+6a^5b^4c^2+11a^5b^4c+9a^5b^4+16a^5b^3c^3+28a^5b^3c^2+40a^5b^3c+38a^5b^3+24a^5b^2c^3+48a^5b^2c^2+51a^5b^2c+57a^5b^2+16a^5bc^3+36a^5bc^2+30a^5bc+34a^5b+4a^5c^3+10a^5c^2+8a^5c+10a^5+20a^4b^4c^3+34a^4b^4c^2+45a^4b^4c+40a^4b^4+80a^4b^3c^3+156a^4b^3c^2+160a^4b^3c+170a^4b^3+120a^4b^2c^3+264a^4b^2c^2+195a^4b^2c+246a^4b^2+80a^4bc^3+196a^4bc^2+110a^4bc+136a^4b+20a^4c^3+54a^4c^2+30a^4c+40a^4+40a^3b^4c^3+76a^3b^4c^2+70a^3b^4c+70a^3b^4+160a^3b^3c^3+344a^3b^3c^2+240a^3b^3c+300a^3b^3+240a^3b^2c^3+576a^3b^2c^2+270a^3b^2c+414a^3b^2+160a^3bc^3+424a^3bc^2+140a^3bc+204a^3b+40a^3c^3+116a^3c^2+40a^3c+60a^3+40a^2b^4c^3+84a^2b^4c^2+48a^2b^4c+58a^2b^4+160a^2b^3c^3+376a^2b^3c^2+152a^2b^3c+248a^2b^3+240a^2b^2c^3+624a^2b^2c^2+138a^2b^2c+312a^2b^2+160a^2bc^3+456a^2bc^2+52a^2bc+111a^2b+40a^2c^3+124a^2c^2+18a^2c+33a^2+20ab^4c^3+46ab^4c^2+15ab^4c+19ab^4+80ab^3c^3+204ab^3c^2+40ab^3c+82ab^3+120ab^2c^3+336ab^2c^2+15ab^2c+81ab^2+80abc^3+244abc^2+20ac^3+66ac^2+4b^4c^3+10b^4c^2+3b^4c+4b^4+16b^3c^3+44b^3c^2+8b^3c+18b^3+24b^2c^3+72b^2c^2+3b^2c+16b^2+16bc^3+47bc^2+4c^3+13c^2  $$\n",
+      "The sum of all inequalities gives us a proof of the inequality.\n",
+      "\n",
+      "\\hline\n",
+      "\n",
+      "Substitute $a\\to 1+a,b\\to 1+b,c\\to 1/(1+c)$\n",
+      "Numerator after substitutions: 4a^5c^3+12a^5c^2+12a^5c+4a^5+4a^4bc^3+12a^4bc^2+12a^4bc+4a^4b+18a^4c^3+58a^4c^2+62a^4c+22a^4+12a^3bc^3+36a^3bc^2+36a^3bc+12a^3b+28a^3c^3+98a^3c^2+112a^3c+42a^3+12a^2bc^3+36a^2bc^2+36a^2bc+12a^2b+16a^2c^3+66a^2c^2+84a^2c+34a^2+4ab^3c^3+12ab^3c^2+12ab^3c+4ab^3+3ab^2c^3+9ab^2c^2+9ab^2c+3ab^2-2abc^3-6abc^2-6abc-2ab+4ac^3+4ac^2+4b^4c^3+12b^4c^2+12b^4c+4b^4+14b^3c^3+46b^3c^2+50b^3c+18b^3+9b^2c^3+36b^2c^2+45b^2c+18b^2+2bc^3-2bc+10c^3+14c^2\n",
+      "status: 0\n",
+      "From weighted AM-GM inequality:\n",
+      "$$6abc \\le 2a^3+2b^2+2bc^3$$\n",
+      "$$2ab \\le a^2+b^2$$\n",
+      "$$2bc \\le b^2+c^2$$\n",
+      "$$6abc^2 \\le 3a^2c^2+2b^2c^3+b^2$$\n",
+      "$$2abc^3 \\le a^2c^3+b^2c^3$$\n",
+      "\n",
+      "$$  0  \\le \n",
+      "4a^5c^3+12a^5c^2+12a^5c+4a^5+4a^4bc^3+12a^4bc^2+12a^4bc+4a^4b+18a^4c^3+58a^4c^2+62a^4c+22a^4+12a^3bc^3+36a^3bc^2+36a^3bc+12a^3b+28a^3c^3+98a^3c^2+112a^3c+40a^3+12a^2bc^3+36a^2bc^2+36a^2bc+12a^2b+15a^2c^3+63a^2c^2+84a^2c+33a^2+4ab^3c^3+12ab^3c^2+12ab^3c+4ab^3+3ab^2c^3+9ab^2c^2+9ab^2c+3ab^2+4ac^3+4ac^2+4b^4c^3+12b^4c^2+12b^4c+4b^4+14b^3c^3+46b^3c^2+50b^3c+18b^3+6b^2c^3+36b^2c^2+45b^2c+13b^2+10c^3+13c^2  $$\n",
+      "The sum of all inequalities gives us a proof of the inequality.\n",
+      "\n",
+      "\\hline\n",
+      "\n",
+      "Substitute $a\\to 1/(1+a),b\\to 1+b,c\\to 1/(1+c)$\n",
+      "Numerator after substitutions: 4a^5b^4c^3+12a^5b^4c^2+12a^5b^4c+4a^5b^4+10a^5b^3c^3+34a^5b^3c^2+38a^5b^3c+14a^5b^3+6a^5b^2c^3+27a^5b^2c^2+36a^5b^2c+15a^5b^2+8a^5bc^3+18a^5bc^2+16a^5bc+6a^5b+8a^5c^3+24a^5c^2+22a^5c+10a^5+20a^4b^4c^3+60a^4b^4c^2+60a^4b^4c+20a^4b^4+54a^4b^3c^3+182a^4b^3c^2+202a^4b^3c+74a^4b^3+33a^4b^2c^3+144a^4b^2c^2+189a^4b^2c+78a^4b^2+34a^4bc^3+72a^4bc^2+62a^4bc+24a^4b+44a^4c^3+114a^4c^2+90a^4c+40a^4+40a^3b^4c^3+120a^3b^4c^2+120a^3b^4c+40a^3b^4+116a^3b^3c^3+388a^3b^3c^2+428a^3b^3c+156a^3b^3+72a^3b^2c^3+306a^3b^2c^2+396a^3b^2c+162a^3b^2+56a^3bc^3+108a^3bc^2+88a^3bc+36a^3b+96a^3c^3+216a^3c^2+140a^3c+60a^3+40a^2b^4c^3+120a^2b^4c^2+120a^2b^4c+40a^2b^4+124a^2b^3c^3+412a^2b^3c^2+452a^2b^3c+164a^2b^3+78a^2b^2c^3+324a^2b^2c^2+414a^2b^2c+168a^2b^2+40a^2bc^3+60a^2bc^2+40a^2bc+20a^2b+100a^2c^3+190a^2c^2+84a^2c+34a^2+20ab^4c^3+60ab^4c^2+60ab^4c+20ab^4+66ab^3c^3+218ab^3c^2+238ab^3c+86ab^3+42ab^2c^3+171ab^2c^2+216ab^2c+87ab^2+12abc^3+6abc^2-4abc+2ab+46ac^3+66ac^2+4b^4c^3+12b^4c^2+12b^4c+4b^4+14b^3c^3+46b^3c^2+50b^3c+18b^3+9b^2c^3+36b^2c^2+45b^2c+18b^2+2bc^3-2bc+10c^3+14c^2\n",
+      "status: 0\n",
+      "From weighted AM-GM inequality:\n",
+      "$$2bc \\le b^2+c^2$$\n",
+      "$$4abc \\le 2a^2+b^4c^2+c^2$$\n",
+      "\n",
+      "$$  0  \\le \n",
+      "4a^5b^4c^3+12a^5b^4c^2+12a^5b^4c+4a^5b^4+10a^5b^3c^3+34a^5b^3c^2+38a^5b^3c+14a^5b^3+6a^5b^2c^3+27a^5b^2c^2+36a^5b^2c+15a^5b^2+8a^5bc^3+18a^5bc^2+16a^5bc+6a^5b+8a^5c^3+24a^5c^2+22a^5c+10a^5+20a^4b^4c^3+60a^4b^4c^2+60a^4b^4c+20a^4b^4+54a^4b^3c^3+182a^4b^3c^2+202a^4b^3c+74a^4b^3+33a^4b^2c^3+144a^4b^2c^2+189a^4b^2c+78a^4b^2+34a^4bc^3+72a^4bc^2+62a^4bc+24a^4b+44a^4c^3+114a^4c^2+90a^4c+40a^4+40a^3b^4c^3+120a^3b^4c^2+120a^3b^4c+40a^3b^4+116a^3b^3c^3+388a^3b^3c^2+428a^3b^3c+156a^3b^3+72a^3b^2c^3+306a^3b^2c^2+396a^3b^2c+162a^3b^2+56a^3bc^3+108a^3bc^2+88a^3bc+36a^3b+96a^3c^3+216a^3c^2+140a^3c+60a^3+40a^2b^4c^3+120a^2b^4c^2+120a^2b^4c+40a^2b^4+124a^2b^3c^3+412a^2b^3c^2+452a^2b^3c+164a^2b^3+78a^2b^2c^3+324a^2b^2c^2+414a^2b^2c+168a^2b^2+40a^2bc^3+60a^2bc^2+40a^2bc+20a^2b+100a^2c^3+190a^2c^2+84a^2c+32a^2+20ab^4c^3+60ab^4c^2+60ab^4c+20ab^4+66ab^3c^3+218ab^3c^2+238ab^3c+86ab^3+42ab^2c^3+171ab^2c^2+216ab^2c+87ab^2+12abc^3+6abc^2+2ab+46ac^3+66ac^2+4b^4c^3+11b^4c^2+12b^4c+4b^4+14b^3c^3+46b^3c^2+50b^3c+18b^3+9b^2c^3+36b^2c^2+45b^2c+17b^2+2bc^3+10c^3+12c^2  $$\n",
+      "The sum of all inequalities gives us a proof of the inequality.\n",
+      "\n",
+      "\\hline\n",
+      "\n",
+      "Substitute $a\\to 1+a,b\\to 1/(1+b),c\\to 1/(1+c)$\n"
+     ]
+    },
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "Numerator after substitutions: 4a^5b^4c^3+12a^5b^4c^2+12a^5b^4c+4a^5b^4+16a^5b^3c^3+48a^5b^3c^2+48a^5b^3c+16a^5b^3+24a^5b^2c^3+72a^5b^2c^2+72a^5b^2c+24a^5b^2+16a^5bc^3+48a^5bc^2+48a^5bc+16a^5b+4a^5c^3+12a^5c^2+12a^5c+4a^5+14a^4b^4c^3+46a^4b^4c^2+50a^4b^4c+18a^4b^4+60a^4b^3c^3+196a^4b^3c^2+212a^4b^3c+76a^4b^3+96a^4b^2c^3+312a^4b^2c^2+336a^4b^2c+120a^4b^2+68a^4bc^3+220a^4bc^2+236a^4bc+84a^4b+18a^4c^3+58a^4c^2+62a^4c+22a^4+16a^3b^4c^3+62a^3b^4c^2+76a^3b^4c+30a^3b^4+76a^3b^3c^3+284a^3b^3c^2+340a^3b^3c+132a^3b^3+132a^3b^2c^3+480a^3b^2c^2+564a^3b^2c+216a^3b^2+100a^3bc^3+356a^3bc^2+412a^3bc+156a^3b+28a^3c^3+98a^3c^2+112a^3c+42a^3+4a^2b^4c^3+30a^2b^4c^2+48a^2b^4c+22a^2b^4+28a^2b^3c^3+156a^2b^3c^2+228a^2b^3c+100a^2b^3+60a^2b^2c^3+288a^2b^2c^2+396a^2b^2c+168a^2b^2+52a^2bc^3+228a^2bc^2+300a^2bc+124a^2b+16a^2c^3+66a^2c^2+84a^2c+34a^2+5ab^4c^3+7ab^4c^2+3ab^4c+ab^4+24ab^3c^3+40ab^3c^2+24ab^3c+8ab^3+33ab^2c^3+51ab^2c^2+27ab^2c+9ab^2+18abc^3+22abc^2+6abc+2ab+4ac^3+4ac^2+7b^4c^3+16b^4c^2+9b^4c+4b^4+38b^3c^3+82b^3c^2+46b^3c+18b^3+63b^2c^3+120b^2c^2+51b^2c+18b^2+38bc^3+56bc^2+2bc+10c^3+14c^2\n",
+      "status: 0\n",
+      "\n",
+      "$$  0  \\le \n",
+      "4a^5b^4c^3+12a^5b^4c^2+12a^5b^4c+4a^5b^4+16a^5b^3c^3+48a^5b^3c^2+48a^5b^3c+16a^5b^3+24a^5b^2c^3+72a^5b^2c^2+72a^5b^2c+24a^5b^2+16a^5bc^3+48a^5bc^2+48a^5bc+16a^5b+4a^5c^3+12a^5c^2+12a^5c+4a^5+14a^4b^4c^3+46a^4b^4c^2+50a^4b^4c+18a^4b^4+60a^4b^3c^3+196a^4b^3c^2+212a^4b^3c+76a^4b^3+96a^4b^2c^3+312a^4b^2c^2+336a^4b^2c+120a^4b^2+68a^4bc^3+220a^4bc^2+236a^4bc+84a^4b+18a^4c^3+58a^4c^2+62a^4c+22a^4+16a^3b^4c^3+62a^3b^4c^2+76a^3b^4c+30a^3b^4+76a^3b^3c^3+284a^3b^3c^2+340a^3b^3c+132a^3b^3+132a^3b^2c^3+480a^3b^2c^2+564a^3b^2c+216a^3b^2+100a^3bc^3+356a^3bc^2+412a^3bc+156a^3b+28a^3c^3+98a^3c^2+112a^3c+42a^3+4a^2b^4c^3+30a^2b^4c^2+48a^2b^4c+22a^2b^4+28a^2b^3c^3+156a^2b^3c^2+228a^2b^3c+100a^2b^3+60a^2b^2c^3+288a^2b^2c^2+396a^2b^2c+168a^2b^2+52a^2bc^3+228a^2bc^2+300a^2bc+124a^2b+16a^2c^3+66a^2c^2+84a^2c+34a^2+5ab^4c^3+7ab^4c^2+3ab^4c+ab^4+24ab^3c^3+40ab^3c^2+24ab^3c+8ab^3+33ab^2c^3+51ab^2c^2+27ab^2c+9ab^2+18abc^3+22abc^2+6abc+2ab+4ac^3+4ac^2+7b^4c^3+16b^4c^2+9b^4c+4b^4+38b^3c^3+82b^3c^2+46b^3c+18b^3+63b^2c^3+120b^2c^2+51b^2c+18b^2+38bc^3+56bc^2+2bc+10c^3+14c^2  $$\n",
+      "The sum of all inequalities gives us a proof of the inequality.\n",
+      "\n",
+      "\\hline\n",
+      "\n",
+      "Substitute $a\\to 1/(1+a),b\\to 1/(1+b),c\\to 1/(1+c)$\n",
+      "Numerator after substitutions: 11a^5b^4c^2+16a^5b^4c+9a^5b^4+10a^5b^3c^3+62a^5b^3c^2+74a^5b^3c+38a^5b^3+30a^5b^2c^3+117a^5b^2c^2+120a^5b^2c+57a^5b^2+24a^5bc^3+78a^5bc^2+72a^5bc+34a^5b+8a^5c^3+24a^5c^2+22a^5c+10a^5+9a^4b^4c^3+64a^4b^4c^2+75a^4b^4c+40a^4b^4+86a^4b^3c^3+346a^4b^3c^2+350a^4b^3c+170a^4b^3+195a^4b^2c^3+612a^4b^2c^2+543a^4b^2c+246a^4b^2+142a^4bc^3+384a^4bc^2+298a^4bc+136a^4b+44a^4c^3+114a^4c^2+90a^4c+40a^4+36a^3b^4c^3+146a^3b^4c^2+140a^3b^4c+70a^3b^4+244a^3b^3c^3+764a^3b^3c^2+660a^3b^3c+300a^3b^3+480a^3b^2c^3+1278a^3b^2c^2+972a^3b^2c+414a^3b^2+328a^3bc^3+756a^3bc^2+472a^3bc+204a^3b+96a^3c^3+216a^3c^2+140a^3c+60a^3+54a^2b^4c^3+162a^2b^4c^2+126a^2b^4c+58a^2b^4+312a^2b^3c^3+816a^2b^3c^2+592a^2b^3c+248a^2b^3+558a^2b^2c^3+1284a^2b^2c^2+798a^2b^2c+312a^2b^2+360a^2bc^3+700a^2bc^2+296a^2bc+116a^2b+100a^2c^3+190a^2c^2+84a^2c+34a^2+30ab^4c^3+73ab^4c^2+42ab^4c+19ab^4+166ab^3c^3+370ab^3c^2+206ab^3c+82ab^3+282ab^2c^3+549ab^2c^2+228ab^2c+81ab^2+172abc^3+258abc^2+4abc-2ab+46ac^3+66ac^2+7b^4c^3+16b^4c^2+9b^4c+4b^4+38b^3c^3+82b^3c^2+46b^3c+18b^3+63b^2c^3+120b^2c^2+51b^2c+18b^2+38bc^3+56bc^2+2bc+10c^3+14c^2\n",
+      "status: 0\n",
+      "From weighted AM-GM inequality:\n",
+      "$$2ab \\le a^2+b^2$$\n",
+      "\n",
+      "$$  0  \\le \n",
+      "11a^5b^4c^2+16a^5b^4c+9a^5b^4+10a^5b^3c^3+62a^5b^3c^2+74a^5b^3c+38a^5b^3+30a^5b^2c^3+117a^5b^2c^2+120a^5b^2c+57a^5b^2+24a^5bc^3+78a^5bc^2+72a^5bc+34a^5b+8a^5c^3+24a^5c^2+22a^5c+10a^5+9a^4b^4c^3+64a^4b^4c^2+75a^4b^4c+40a^4b^4+86a^4b^3c^3+346a^4b^3c^2+350a^4b^3c+170a^4b^3+195a^4b^2c^3+612a^4b^2c^2+543a^4b^2c+246a^4b^2+142a^4bc^3+384a^4bc^2+298a^4bc+136a^4b+44a^4c^3+114a^4c^2+90a^4c+40a^4+36a^3b^4c^3+146a^3b^4c^2+140a^3b^4c+70a^3b^4+244a^3b^3c^3+764a^3b^3c^2+660a^3b^3c+300a^3b^3+480a^3b^2c^3+1278a^3b^2c^2+972a^3b^2c+414a^3b^2+328a^3bc^3+756a^3bc^2+472a^3bc+204a^3b+96a^3c^3+216a^3c^2+140a^3c+60a^3+54a^2b^4c^3+162a^2b^4c^2+126a^2b^4c+58a^2b^4+312a^2b^3c^3+816a^2b^3c^2+592a^2b^3c+248a^2b^3+558a^2b^2c^3+1284a^2b^2c^2+798a^2b^2c+312a^2b^2+360a^2bc^3+700a^2bc^2+296a^2bc+116a^2b+100a^2c^3+190a^2c^2+84a^2c+33a^2+30ab^4c^3+73ab^4c^2+42ab^4c+19ab^4+166ab^3c^3+370ab^3c^2+206ab^3c+82ab^3+282ab^2c^3+549ab^2c^2+228ab^2c+81ab^2+172abc^3+258abc^2+4abc+46ac^3+66ac^2+7b^4c^3+16b^4c^2+9b^4c+4b^4+38b^3c^3+82b^3c^2+46b^3c+18b^3+63b^2c^3+120b^2c^2+51b^2c+17b^2+38bc^3+56bc^2+2bc+10c^3+14c^2  $$\n",
+      "The sum of all inequalities gives us a proof of the inequality.\n"
+     ]
+    }
+   ],
+   "source": [
+    "formula=Sm('-(3a + 2b + c)(2a^3 + 3b^2 + 6c + 1) + (4a + 4b + 4c)(a^4 + b^3 + c^2 + 3)')\n",
+    "powerprove(formula)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Now let's take a look at slightly another kind of the problem.\n",
+    "#### Problem\n",
+    "Let $f:R^3\\to R$ be a convex function. Prove that\n",
+    "$$f(1,2,3)+f(2,3,1)+f(3,1,2)\\le f(4,3,-1)+f(3,-1,4)+f(-1,4,3).$$\n",
+    "\n",
+    "To create a proof, we will use `provef` function. It assumes that $f$ is convex and nonnegative, then it tries to find a proof. However, if the last inequality is $0\\le 0$, then the proof works for any convex function."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 31,
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "numerator: $$21f(-1,4,3)-21f(1,2,3)-21f(2,3,1)+21f(3,-1,4)-21f(3,1,2)+21f(4,3,-1)$$\n",
+      "denominator: $$1$$\n",
+      "status: 0\n",
+      "From Jensen inequality:\n",
+      "$$21f(1, 2, 3) \\le 11f(-1, 4, 3)+8f(3, -1, 4)+2f(4, 3, -1)$$\n",
+      "$$21f(2, 3, 1) \\le 8f(-1, 4, 3)+2f(3, -1, 4)+11f(4, 3, -1)$$\n",
+      "$$21f(3, 1, 2) \\le 2f(-1, 4, 3)+11f(3, -1, 4)+8f(4, 3, -1)$$\n",
+      "\n",
+      "$$  0  \\le \n",
+      "0  $$\n",
+      "The sum of all inequalities gives us a proof of the inequality.\n"
+     ]
+    }
+   ],
+   "source": [
+    "provef('(-f(1,2,3)-f(2,3,1)-f(3,1,2)+f(4,3,-1)+f(3,-1,4)+f(-1,4,3))*21')"
+   ]
+  },
   {
    "cell_type": "code",
    "execution_count": null,

shiroindev.py

@@ -15,7 +15,7 @@ translationList=['numerator:','denominator:','status:',
 "Program couldn't find any proof.",
 "Try to set higher linprogiter parameter.",
 "It looks like the formula is symmetric. You can assume without loss of"+
-" generality that ","Try"
+" generality that ","Try", 'From Jensen inequality:'
 ]
 #Initialize english-english dictionary.
 for phrase in translationList:
@@ -123,7 +123,7 @@ def _formula2list(formula,variables):
 			rcoef+=[coef]
 			rfun+=[powers]
 	return(lcoef,lfun,rcoef,rfun)
-def _list2proof(lcoef,lfun,rcoef,rfun,variables,itermax,linprogiter,_writ2=_writ2):
+def _list2proof(lcoef,lfun,rcoef,rfun,variables,itermax,linprogiter,_writ2=_writ2,theorem="From weighted AM-GM inequality:"):
 #Now the formula is splitted on two polynomials with positive coefficients.
 #we will call them LHS and RHS and our inequality to prove would
 #be LHS<=RHS (instead of 0<=RHS-LHS).
@@ -198,7 +198,7 @@ def _list2proof(lcoef,lfun,rcoef,rfun,variables,itermax,linprogiter,_writ2=_writ
 		if itern==1:
 			print(sTranslation['status:'],status)
 			if status==0:
-				print(sTranslation['From weighted AM-GM inequality:'])
+				print(sTranslation[theorem])
 		if status==2: #if real solution of current inequality doesn't exist
 			if foundreal==0: #if this is the first inequality, then break 
 				break
@@ -397,7 +397,7 @@ def provef(formula,niter=200,linprogiter=10000):
 #provides a proof of nonnegativity.
 	formula=S(formula)
 	num,den=_input2fraction(formula,[],[])
-	_list2proof(*(_formula2listf(num)+(None,niter,linprogiter,_writ)))
+	_list2proof(*(_formula2listf(num)+(None,niter,linprogiter,_writ,'From Jensen inequality:')))
 def issymetric(formula): #checks if formula is symmetric
 #and has at least two variables	
 	if len(formula.free_symbols)<2: