pretty printing

This commit is contained in:
urojony 2020-04-16 08:58:06 +02:00
parent 5832f57474
commit a7167126e5
5 changed files with 2777 additions and 424 deletions

View File

@ -2,12 +2,14 @@
"cells": [
{
"cell_type": "code",
"execution_count": 1,
"execution_count": 7,
"metadata": {},
"outputs": [],
"source": [
"from shiroindev import *\n",
"sSeed=1"
"sSeed=1\n",
"from IPython.display import Latex\n",
"sPrint=lambda x:display(Latex(x))"
]
},
{
@ -36,21 +38,20 @@
},
{
"cell_type": "code",
"execution_count": 2,
"execution_count": 8,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"numerator: $$a^2-ab-ac+b^2-bc+c^2$$\n",
"denominator: $$1$$\n",
"numerator: $a^2-ab-ac+b^2-bc+c^2$\n",
"denominator: $1$\n",
"status: 0\n",
"From weighted AM-GM inequality:\n",
"\n",
"Program couldn't find a solution with integer coefficients. Try to multiple the formula by some integer and run this function again.\n",
"$$ ab+ac+bc \\le \n",
"a^2+b^2+c^2 $$\n"
"$$ ab+ac+bc \\le a^2+b^2+c^2 $$\n"
]
},
{
@ -59,7 +60,7 @@
"0"
]
},
"execution_count": 2,
"execution_count": 8,
"metadata": {},
"output_type": "execute_result"
}
@ -759,10 +760,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 +782,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": 33,
"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 2a^3c+2a^2+2b^3+4bc^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+38a^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+31a^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+16b^3+24b^2c^3+72b^2c^2+3b^2c+16b^2+16bc^3+48bc^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",
"$$2ab \\le a^2+b^2$$\n",
"$$2bc \\le b^2+c^2$$\n",
"$$6abc \\le 3a^2c+3b^2c$$\n",
"$$2abc^3 \\le a^2bc^3+bc^3$$\n",
"$$6abc^2 \\le a^4b+a^2c^3+b^4c^2+bc^3+2c^2$$\n",
"\n",
"$$ 0 \\le \n",
"4a^5c^3+12a^5c^2+12a^5c+4a^5+4a^4bc^3+12a^4bc^2+12a^4bc+3a^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+11a^2bc^3+36a^2bc^2+36a^2bc+12a^2b+15a^2c^3+66a^2c^2+81a^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+11b^4c^2+12b^4c+4b^4+14b^3c^3+46b^3c^2+50b^3c+18b^3+9b^2c^3+36b^2c^2+42b^2c+16b^2+10c^3+11c^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 a^2c^2+2ab^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+189a^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+85ab^2+12abc^3+6abc^2+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+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",
"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"
]
},
{
"name": "stdout",
"output_type": "stream",
"text": [
"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,

Binary file not shown.

File diff suppressed because it is too large Load Diff

View File

@ -4,8 +4,12 @@ import warnings,operator
warnings.filterwarnings("ignore")
#Seed is needed to select the weights in linprog function.
#None means that the seed is random.
sSeed=None
sTranslation={}
class Empty:
pass
sVars=Empty()
sVars.print=print
sVars.seed=None
sVars.translation={}
translationList=['numerator:','denominator:','status:',
'Substitute',"Formula after substitution:",
"Numerator after substitutions:","From weighted AM-GM inequality:",
@ -19,7 +23,7 @@ translationList=['numerator:','denominator:','status:',
]
#Initialize english-english dictionary.
for phrase in translationList:
sTranslation[phrase]=phrase
sVars.translation[phrase]=phrase
from scipy.optimize import linprog
import random
from sympy import S,cancel,fraction,Pow,expand,solve,latex
@ -84,12 +88,12 @@ def _input2fraction(formula,variables,values):
subst=[]
for x,y in zip(variables,values):
if y!=1:
print(sTranslation['Substitute'],'$',x,'\\to',slatex(S(y)*S(x)),'$')
sVars.print(sVars.translation['Substitute']+' $'+str(x)+'\\to '+slatex(S(y)*S(x))+'$')
subst+=[(x,x*y)]
formula=formula.subs(subst)
numerator,denominator=fractioncancel(formula)
print(sTranslation['numerator:'],'$$'+slatex(numerator)+'$$')
print(sTranslation['denominator:'],'$$'+slatex(denominator)+'$$')
sVars.print(sVars.translation['numerator:']+' $'+slatex(numerator)+'$')
sVars.print(sVars.translation['denominator:']+' $'+slatex(denominator)+'$')
return (numerator,denominator)
def _formula2list(formula,variables):
#Splits a polynomial to a difference of two polynomials with positive
@ -151,15 +155,15 @@ def _list2proof(lcoef,lfun,rcoef,rfun,variables,itermax,linprogiter,_writ2=_writ
#If there are some inequalities with all integer coefficients, subtract
#them from the original one.
#If LHS is empty, then break.
localseed=sSeed
localseed=sVars.seed
bufer=''
itern=0
if len(lcoef)==0: #if LHS is empty
print(sTranslation['status:'], 0)
sVars.print(sVars.translation['status:']+' 0')
status=0
elif len(rcoef)==0:
#if RHS is empty, but LHS is not
print(sTranslation['status:'], 2)
sVars.print(sVars.translation['status:']+' 2')
status=2
itermax=0
foundreal=0
@ -196,9 +200,9 @@ def _list2proof(lcoef,lfun,rcoef,rfun,variables,itermax,linprogiter,_writ2=_writ
res=linprog(vecc,A_eq=A,b_eq=b,A_ub=A_ub,b_ub=b_ub,options={'maxiter':linprogiter})
status=res.status
if itern==1:
print(sTranslation['status:'],status)
sVars.print(sVars.translation['status:']+' '+str(status))
if status==0:
print(sTranslation[theorem])
sVars.print(sVars.translation[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
@ -209,7 +213,8 @@ def _list2proof(lcoef,lfun,rcoef,rfun,variables,itermax,linprogiter,_writ2=_writ
bufer=''
continue
if status==0:#if found a solution with real coefficients
print(bufer,end='')
if bufer:
sVars.print(bufer)
foundreal=1
bufer=''
oldlfun,oldrfun=lfun,rfun
@ -236,29 +241,28 @@ def _list2proof(lcoef,lfun,rcoef,rfun,variables,itermax,linprogiter,_writ2=_writ
if(c):bufer+='+'
else:c=1
bufer+=_writ2(int(round(j)),k,variables)
bufer+='$$\n'
bufer+='$$'
lcoef,lfun=_remzero(lcoef,lfun)
rcoef,rfun=_remzero(rcoef,rfun)
print(bufer)
sVars.print(bufer)
lhs='+'.join([_writ2(c,f,variables) for c,f in zip(lcoef,lfun)])
if lhs=='':
lhs='0'
elif status==0:
print(sTranslation[
sVars.print(sVars.translation[
"Program couldn't find a solution with integer coefficients. Try "+
"to multiple the formula by some integer and run this function again."])
elif(status==2):
print(sTranslation["Program couldn't find any proof."])
sVars.print(sVars.translation["Program couldn't find any proof."])
#return res.status
elif status==1:
print(sTranslation["Try to set higher linprogiter parameter."])
print('$$ ',slatex(lhs),' \\le ')
sVars.print(sVars.translation["Try to set higher linprogiter parameter."])
rhs='+'.join([_writ2(c,f,variables) for c,f in zip(rcoef,rfun)])
if rhs=='':
rhs='0'
print(slatex(rhs),' $$')
sVars.print('$$ '+slatex(lhs)+' \\le '+slatex(rhs)+' $$')
if lhs=='0':
print(sTranslation['The sum of all inequalities gives us a proof of the inequality.'])
sVars.print(sVars.translation['The sum of all inequalities gives us a proof of the inequality.'])
return status
def _isiterable(obj):
try:
@ -287,11 +291,11 @@ def prove(formula,values=None,variables=None,niter=200,linprogiter=10000):
st=_list2proof(*(_formula2list(num,variables)+(variables,niter,linprogiter)))
if st==2 and issymetric(num):
fs=sorted([str(x) for x in num.free_symbols])
print(sTranslation["It looks like the formula is symmetric. "+
"You can assume without loss of generality that "],
' >= '.join([str(x) for x in fs]),sTranslation['Try'])
print('prove(makesubs(S("',num,'"),',
[(str(x),'inf') for x in variables[1:]],')')
sVars.print(sVars.translation["It looks like the formula is symmetric. "+
"You can assume without loss of generality that "]+
' >= '.join([str(x) for x in fs])+'. '+sVars.translation['Try'])
sVars.print('prove(makesubs(S("'+str(num)+'"),'+
str([(str(x),'inf') for x in variables[1:]])+')')
return st
def powerprove(formula,values=None,variables=None,niter=200,linprogiter=10000):
#This is a bruteforce and ineffective function for proving inequalities.
@ -306,7 +310,7 @@ def powerprove(formula,values=None,variables=None,niter=200,linprogiter=10000):
for j in range(len(variables)):
subst2+=[(variables[j],1+variables[j])]
for i in range(1<<len(variables)): #tricky substitutions to improve speed
print('\n\\hline\n')
sVars.print('\n\\hline\n')
subst1=[]
substout=[]
for j in range(len(variables)):
@ -315,10 +319,10 @@ def powerprove(formula,values=None,variables=None,niter=200,linprogiter=10000):
substout+=[str(variables[j])+'\\to 1/(1+'+str(variables[j])+')']
else:
substout+=[str(variables[j])+'\\to 1+'+str(variables[j])]
print(sTranslation['Substitute'], '$'+','.join(substout)+'$')
sVars.print(sVars.translation['Substitute']+ ' $'+','.join(substout)+'$')
num1=fractioncancel(num.subs(subst1))[0]
num2=expand(num1.subs(subst2))
print(sTranslation["Numerator after substitutions:"],slatex(num2))
sVars.print(sVars.translation["Numerator after substitutions:"]+' $'+slatex(num2)+'$')
_list2proof(*(_formula2list(num2,variables)+(variables,niter,linprogiter)))
def makesubs(formula,intervals,values=None,variables=None,numden=False):
#This function generates a new formula which satisfies this condition:
@ -340,18 +344,18 @@ def makesubs(formula,intervals,values=None,variables=None,numden=False):
if {end1,end2}=={S('-inf'),S('inf')}:
formula=formula.subs(var,var-1/var)
equations=[equation.subs(var,var-1/var) for equation in equations]
print(sTranslation['Substitute'],'$',var,'\\to',var-1/var,'$')
sVars.print(sVars.translation['Substitute']+' $'+str(var)+'\\to '+var-1/var+'$')
elif end2==S('inf'):
formula=formula.subs(var,end1+var)
equations=[equation.subs(var,end1+var) for equation in equations]
print(sTranslation['Substitute'],'$',var,'\\to',sstr(end1+var),'$')
sVars.print(sVars.translation['Substitute']+' $'+str(var)+'\\to '+sstr(end1+var)+'$')
elif end2==S('-inf'):
formula=formula.subs(var,end1-var)
equations=[equation.subs(var,end1-var) for equation in equations]
print(sTranslation['Substitute'], "$",var,'\\to',sstr(end1-var),'$')
sVars.print(sVars.translation['Substitute']+" $"+str(var)+'\\to '+sstr(end1-var)+'$')
else:
formula=formula.subs(var,end2+(end1-end2)/var)
print(sTranslation['Substitute'], "$",var,'\\to',sstr(end2+(end1-end2)/(1+var)),'$')
sVars.print(sVars.translation['Substitute']+" $"+str(var)+'\\to '+sstr(end2+(end1-end2)/(1+var))+'$')
equations=[equation.subs(var,end2+(end1-end2)/var) for equation in equations]
num,den=fractioncancel(formula)
for var,interval in zip(variables,intervals):
@ -364,7 +368,7 @@ def makesubs(formula,intervals,values=None,variables=None,numden=False):
if len(values):
values=values[0]
num,den=expand(num),expand(den)
#print(sTranslation["Formula after substitution:"],"$$",slatex(num/den),'$$')
#sVars.print(sVars.translation["Formula after substitution:"],"$$",slatex(num/den),'$$')
if values and numden:
return num,den,values
elif values: