adamski/shiroindev
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

first commit

Browse Source
This commit is contained in:
urojony 2020-04-10 22:44:54 +02:00
parent 6a8d5fe394
commit 0cbb73e980
4 changed files with 2090 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

824
.ipynb_checkpoints/examples-checkpoint.ipynb Normal file
View File

@ -0,0 +1,824 @@
{
"cells": [
{
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [
{
"name": "stderr",
"output_type": "stream",
"text": [
"/home/grzegorz/shiroindev/shiroindev.py:40: DeprecationWarning: invalid escape sequence \\^\n",
" formula=re.sub('\\^{(.)}',r'^\\1',latex(formula,fold_short_frac=True).replace(' ','').replace('\\\\left(','(').replace('\\\\right)',')'))\n",
"/home/grzegorz/shiroindev/shiroindev.py:41: DeprecationWarning: invalid escape sequence \\{\n",
" return re.sub('\\{(\\(.+?\\))\\}',r'\\1',formula)\n"
]
}
],
"source": [
"from shiroindev import *\n",
"sSeed=1"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The first line obviously loads this package. The second one sets a seed for proving functions. If you don't write it, you can get slightly different proof each time you run a function. \n",
"\n",
"Now let's make some proofs. We will use problems from https://www.imomath.com/index.php?options=593&lmm=0."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Problem 1\n",
"Prove the inequality $a^2+b^2+c^2\\ge ab+bc+ca$, if $a,b,c$ are real numbers."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Function `prove` tries to prove that given formula is nonnegative, **assuming all variables are nonnegative**. In this case the nonnegativity assumption is not a problem, since all powers on the left side are even, so if $|a|^2+|b|^2+|c|^2 \\ge |ab|+|ac|+|bc|,$ then $a^2+b^2+c^2= |a|^2+|b|^2+|c|^2 \\ge |ab|+|ac|+|bc| \\ge ab+ac+bc$."
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"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"
]
},
{
"data": {
"text/plain": [
"0"
]
},
"execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"prove('(a^2+b^2+c^2-a*b-a*c-b*c)')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Function prove prints several things. The first two gives us a formula after expanding it. To proceed, a **numerator** has to be a **polynomial with integer coefficients**. The next one is status, which is the return status of the first use of ```scipy.optimize.linprog```. Possible outputs and explanations are\n",
"\n",
"* 0 - found a proof with real coefficients,\n",
"* 1 - need more time, \n",
"* 2 - function didn't find a proof,\n",
"* 3,4 - loss of precision (which may happen if it has to work with big numbers).\n",
"\n",
"Then we've got a hint. So let's use it!"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"numerator: $$2a^2-2ab-2ac+2b^2-2bc+2c^2$$\n",
"denominator: $$1$$\n",
"status: 0\n",
"From weighted AM-GM inequality:\n",
"$$2ab \\le a^2+b^2$$\n",
"$$2ac \\le a^2+c^2$$\n",
"$$2bc \\le b^2+c^2$$\n",
"\n",
"$$ 0 \\le \n",
"0 $$\n",
"The sum of all inequalities gives us a proof of the inequality.\n"
]
},
{
"data": {
"text/plain": [
"0"
]
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"prove('(a^2+b^2+c^2-a*b-a*c-b*c)*2')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Problem 2\n",
"Find all real numbers such that $a^2+b^2+c^2+d^2=a(b+c+d)$. "
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"At first glance it doesn't look like an inequality problem, but actually it is one. If you try to calculate both sides for different values, you can see that the left side of the equation is never less than the right one. So let's try"
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"numerator: $$a^2-ab-ac-ad+b^2+c^2+d^2$$\n",
"denominator: $$1$$\n",
"status: 2\n",
"\n",
"Program couldn't find any proof.\n",
"$$ ab+ac+ad \\le \n",
"a^2+b^2+c^2+d^2 $$\n"
]
},
{
"data": {
"text/plain": [
"2"
]
},
"execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"prove('a^2+b^2+c^2+d^2-a*(b+c+d)')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"This time `prove` didn't found the proof. But it doesn't mean that the inequality is not true! `prove` uses a list of values for which the formula should be small. There is no strict rule here, but the smaller that value is, the higher are chances to find a proof. List of values should correspond to the list of variables in alphabetical order. So let's try $a=2$ and $b=c=d=1$."
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Substitute $ a \\to 2a $\n",
"numerator: $$4a^2-2ab-2ac-2ad+b^2+c^2+d^2$$\n",
"denominator: $$1$$\n",
"status: 0\n",
"From weighted AM-GM inequality:\n",
"$$2ab \\le a^2+b^2$$\n",
"$$2ac \\le a^2+c^2$$\n",
"$$2ad \\le a^2+d^2$$\n",
"\n",
"$$ 0 \\le \n",
"a^2 $$\n",
"The sum of all inequalities gives us a proof of the inequality.\n"
]
},
{
"data": {
"text/plain": [
"0"
]
},
"execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"prove('a^2+b^2+c^2+d^2-a*(b+c+d)','2,1,1,1')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Function makes a substitution $a\\to 2a$ (which should be understood as $a=2a'$) and try to prove new inequality. This time it succeeded. Moreover, if starting formula is equal to 0, then all these inequalities have to be equalities, so $a'^2=0$ and eventually $a=0$. We can also try a little bit lower value for $a$."
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Substitute $ a \\to 7a/4 $\n",
"numerator: $$49a^2-28ab-28ac-28ad+16b^2+16c^2+16d^2$$\n",
"denominator: $$16$$\n",
"status: 0\n",
"From weighted AM-GM inequality:\n",
"$$28ab \\le 14a^2+14b^2$$\n",
"$$28ac \\le 14a^2+14c^2$$\n",
"$$28ad \\le 14a^2+14d^2$$\n",
"\n",
"$$ 0 \\le \n",
"7a^2+2b^2+2c^2+2d^2 $$\n",
"The sum of all inequalities gives us a proof of the inequality.\n"
]
},
{
"data": {
"text/plain": [
"0"
]
},
"execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"prove('a^2+b^2+c^2+d^2-a*(b+c+d)','7/4,1,1,1')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Now we can see that if $a^2+b^2+c^2+d^2-a(b+c+d)=0$, then $7a'^2+2b^2+2c^2+2d^2=0$ and eventually $a=b=c=d=0$. Note that inequality is proved only for positive numbers (which, by continuity, can be expanded to nonnegative numbers). But using similar argumentation to the one in previous problem, if $(a,b,c,d)=(x,y,z,t)$ is the solution of $a^2+b^2+c^2+d^2-a(b+c+d)=0$, then $(a,b,c,d)=(|x|,|y|,|z|,|t|)$ is a solution, too. Since the only nonnegative solution is $(0,0,0,0)$, it means that it is the only solution.\n",
"\n",
"Let's skip the problem 3 and look solve the problem 4 instead.\n",
"\n",
"#### Problem 4\n",
"If $x$ and $y$ are two positive numbers less than 1, prove that\n",
"$$\\frac{1}{1-x^2}+\\frac{1}{1-y^2}\\ge \\frac{2}{1-xy}.$$"
]
},
{
"cell_type": "code",
"execution_count": 7,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"numerator: $$-x^3y+2x^2y^2-x^2-xy^3+2xy-y^2$$\n",
"denominator: $$x^3y^3-x^3y-x^2y^2+x^2-xy^3+xy+y^2-1$$\n",
"status: 2\n",
"\n",
"Program couldn't find any proof.\n",
"$$ x^3y+x^2+xy^3+y^2 \\le \n",
"2x^2y^2+2xy $$\n",
"It looks like the formula is symmetric. You can assume without loss of generality that x >= y Try\n",
"prove(makesubs(S(\" -x**3*y + 2*x**2*y**2 - x**2 - x*y**3 + 2*x*y - y**2 \"), [('y', 'inf')] )\n"
]
},
{
"data": {
"text/plain": [
"2"
]
},
"execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"prove('1/(1-x^2)+1/(1-y^2)-2/(1-x*y)')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"`prove` assumes that formula is well-defined if all variables are positive, so it doesn't have to analyze the denominator (except of choosing the right sign). In this case it is not true, since if $x=1$, then $1-x^2=0$. Also denominator is equal to $(x^2-1)(y^2-1)(xy-1)$ which is negative for $x,y\\in (0,1)$. So we need to make some substitution after which new variables can have all positive values, not just these inside (0,1) interval.\n",
"\n",
"We will use a function `makesubs` to generate these substitutions. It has three basic parameters: `formula`, `intervals` and `values`. `intervals` are current limitations of variables, `values` are values of variables for which `formula` is small. `values` should be inside corresponding `intervals`. This argument is optional but it's better to use it.\n",
"Let's go back to our problem. If $x=y$, then $\\frac{1}{1-x^2}+\\frac{1}{1-y^2}\\ge \\frac{2}{1-xy}$, so it's the minimum value of the formula. So let `values=(1/2,1/2)` (**warning: do not use decimal point**, for example '0.5,0.5')."
]
},
{
"cell_type": "code",
"execution_count": 8,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Substitute $ x \\to 1-1/(x+1) $\n",
"Substitute $ y \\to 1-1/(y+1) $\n",
"numerator: $$6x^3y+3x^3-12x^2y^2-3x^2y+3x^2+6xy^3-3xy^2-6xy+3y^3+3y^2$$\n",
"denominator: $$4x^2y+2x^2+4xy^2+8xy+3x+2y^2+3y+1$$\n",
"status: 0\n",
"From weighted AM-GM inequality:\n",
"$$12x^2y^2 \\le 6x^3y+6xy^3$$\n",
"$$3x^2y \\le 2x^3+y^3$$\n",
"$$3xy^2 \\le x^3+2y^3$$\n",
"$$6xy \\le 3x^2+3y^2$$\n",
"\n",
"$$ 0 \\le \n",
"0 $$\n",
"The sum of all inequalities gives us a proof of the inequality.\n"
]
},
{
"data": {
"text/plain": [
"0"
]
},
"execution_count": 8,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"newformula,newvalues=makesubs('1/(1-x^2)+1/(1-y^2)-2/(1-x*y)','[0,1],[0,1]','1/2,1/2')\n",
"prove(newformula*3,newvalues)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Now let's get back to problem 3.\n",
"\n",
"#### Problem 3\n",
"\n",
"If $a,b,c$ are positive real numbers that satisfy $a^2+b^2+c^2=1$, find the minimal value of\n",
"$$\\frac{a^2b^2}{c^2}+\\frac{b^2c^2}{a^2}+\\frac{c^2a^2}{b^2}$$\n",
"\n",
"The problem is equivalent to finding minimum of $xy/z+yz/x+zx/y$ assuming $x+y+z=1$ and $x,y,z>0$. The first idea is to suppose that the minimum is reached when $x=y=z$. In that case, $x=y=z=1/3$ and formula is equal to 1. Now we can substitute $z\\to 1-x-y$. Constraints for variables are $x>0$, $y>0$, $x+y<1$. We can rewrite it as $x \\in (0,1-y)$, $y \\in (0,1)$. These two conditions have two important properties:\n",
"* constraints for variables are written as intervals,\n",
"* there are no \"backwards dependencies\", i.e. there is no $x$ in the interval of $y$.\n",
"\n",
"If these two conditions hold, then you can use `makesubs` function.\n",
"**Warning:** at this moment `makesubs` **doesn't warn you if your list of intervals doesn't follow these rules!**\n"
]
},
{
"cell_type": "code",
"execution_count": 9,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Substitute $ x \\to -y+1+(y-1)/(x+1) $\n",
"Substitute $ y \\to 1-1/(y+1) $\n",
"Substitute $ y \\to y/2 $\n",
"numerator: $$x^4y^2+x^3y^2-2x^3y-4x^2y+4x^2+xy^2-2xy+y^2$$\n",
"denominator: $$x^3y^2+2x^3y+2x^2y^2+4x^2y+xy^2+2xy$$\n",
"status: 0\n",
"From weighted AM-GM inequality:\n",
"$$2x^3y \\le x^4y^2+x^2$$\n",
"$$4x^2y \\le x^3y^2+2x^2+xy^2$$\n",
"$$2xy \\le x^2+y^2$$\n",
"\n",
"$$ 0 \\le \n",
"0 $$\n",
"The sum of all inequalities gives us a proof of the inequality.\n"
]
},
{
"data": {
"text/plain": [
"0"
]
},
"execution_count": 9,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"formula=Sm('xy/z+yz/x+zx/y-1').subs('z',S('1-x-y'))\n",
"newformula,values=makesubs(formula,'[0,1-y],[0,1]','1/3,1/3')\n",
"prove(newformula,values)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The proof is found, so the assumption that 1 is the minimum of `xy/z+yz/x+zx/y` was good.\n",
"\n",
"Functions `S` and `Sm` creates a SymPy object from a string. The only difference is that `Sm` assumes that there are no multi-letter variables and adds a multiplication sign between every two terms which has no operator sign, so object `Sm(xy/z+yz/x+zx/y)` has 3 variables `x,y,z` and `S('xy/z+yz/x+zx/y')` has 6 variables `x,y,z,xy,yz,zx`. \n",
"\n",
"As you may have noticed, formulas are often cyclic or symmetric. Therefore you can use `cyclize` or `symmetrize` function to reduce the length of the written formula. Here are a few commands which will do the same as each other. "
]
},
{
"cell_type": "code",
"execution_count": 10,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"numerator: $$2a^2-2ab-2ac+2b^2-2bc+2c^2$$\n",
"denominator: $$1$$\n",
"status: 0\n",
"From weighted AM-GM inequality:\n",
"$$2ab \\le a^2+b^2$$\n",
"$$2ac \\le a^2+c^2$$\n",
"$$2bc \\le b^2+c^2$$\n",
"\n",
"$$ 0 \\le \n",
"0 $$\n",
"The sum of all inequalities gives us a proof of the inequality.\n"
]
},
{
"data": {
"text/plain": [
"0"
]
},
"execution_count": 10,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"prove('(a^2+b^2+c^2-a*b-a*c-b*c)*2')\n",
"#prove(S('(a^2+b^2+c^2-a*b-a*c-b*c)*2'))\n",
"#prove(Sm('2(a^2+b^2+c^2-ab-ac-bc)'))\n",
"#prove(cyclize('2*a^2-2*a*b'))\n",
"#prove(symmetrize('a^2-a*b'))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Now look at formula $(x-1)^4$. It's quite obvious that it's nonnegative, but `prove` fails to show this!"
]
},
{
"cell_type": "code",
"execution_count": 11,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"numerator: $$x^4-4x^3+6x^2-4x+1$$\n",
"denominator: $$1$$\n",
"status: 2\n",
"\n",
"Program couldn't find any proof.\n",
"$$ 4x^3+4x \\le \n",
"x^4+6x^2+1 $$\n"
]
},
{
"data": {
"text/plain": [
"2"
]
},
"execution_count": 11,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"prove('(x-1)^4')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"But there is a relatively simple method to generate a proof using this library. We will make to proofs: one for $x\\in (1,\\infty)$ and the second one for $(-\\infty,1)$."
]
},
{
"cell_type": "code",
"execution_count": 12,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Substitute $ x \\to x+1 $\n",
"numerator: $$x^4$$\n",
"denominator: $$1$$\n",
"status: 0\n",
"\n",
"$$ 0 \\le \n",
"x^4 $$\n",
"The sum of all inequalities gives us a proof of the inequality.\n"
]
},
{
"data": {
"text/plain": [
"0"
]
},
"execution_count": 12,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"prove(makesubs('(x-1)^4','(1,inf)'))"
]
},
{
"cell_type": "code",
"execution_count": 13,
"metadata": {
"scrolled": true
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Substitute $ x \\to 1-x $\n",
"numerator: $$x^4$$\n",
"denominator: $$1$$\n",
"status: 0\n",
"\n",
"$$ 0 \\le \n",
"x^4 $$\n",
"The sum of all inequalities gives us a proof of the inequality.\n"
]
},
{
"data": {
"text/plain": [
"0"
]
},
"execution_count": 13,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"prove(makesubs('(x-1)^4','(-inf,1)'))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Now let's go to the problem 10\n",
"#### Problem 10\n",
"If $a,b,c,d>0$, prove that\n",
"$$\\frac a{b+c}+\\frac b{c+d}+ \\frac c{d+a}+ \\frac d{a+b}\\geq 2.$$\n",
"\n",
"Let's try a simple approach."
]
},
{
"cell_type": "code",
"execution_count": 14,
"metadata": {},
"outputs": [
{
"data": {
"text/latex": [
"$\\displaystyle \\frac{a}{b + c} + \\frac{b}{c + d} + \\frac{c}{a + d} + \\frac{d}{a + b} - 2$"
],
"text/plain": [
"a/(b + c) + b/(c + d) + c/(a + d) + d/(a + b) - 2"
]
},
"execution_count": 14,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"formula=cyclize('a/(b+c)',variables='a,b,c,d')-2\n",
"formula"
]
},
{
"cell_type": "code",
"execution_count": 15,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"numerator: $$a^3c+a^3d+a^2b^2-a^2bd-2a^2c^2-a^2cd+a^2d^2+ab^3-ab^2c-ab^2d-abc^2+ac^3-acd^2+b^3d+b^2c^2-2b^2d^2+bc^3-bc^2d-bcd^2+bd^3+c^2d^2+cd^3$$\n",
"denominator: $$a^2bc+a^2bd+a^2c^2+a^2cd+ab^2c+ab^2d+abc^2+2abcd+abd^2+ac^2d+acd^2+b^2cd+b^2d^2+bc^2d+bcd^2$$\n",
"status: 2\n",
"\n",
"Program couldn't find any proof.\n",
"$$ a^2bd+2a^2c^2+a^2cd+ab^2c+ab^2d+abc^2+acd^2+2b^2d^2+bc^2d+bcd^2 \\le \n",
"a^3c+a^3d+a^2b^2+a^2d^2+ab^3+ac^3+b^3d+b^2c^2+bc^3+bd^3+c^2d^2+cd^3 $$\n"
]
},
{
"data": {
"text/plain": [
"2"
]
},
"execution_count": 15,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"prove(formula)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"This problem, like the previous one, can be solved by splitting the domain of variables to several subdomains. But we can also use the symmetry of this inequality. For example, without loss of generality we can assume that $a\\ge c$ and $b\\ge d$, so $a\\in [c,\\infty)$, $b\\in [d,\\infty)$."
]
},
{
"cell_type": "code",
"execution_count": 16,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Substitute $ a \\to a+c $\n",
"Substitute $ b \\to b+d $\n",
"numerator: $$a^3c+a^3d+a^2b^2+a^2bd+a^2c^2+2a^2cd+a^2d^2+ab^3+ab^2c+2ab^2d-abc^2+abd^2+b^3c+b^3d+b^2c^2+2b^2cd+b^2d^2$$\n",
"denominator: $$a^2bc+a^2bd+a^2c^2+2a^2cd+a^2d^2+ab^2c+ab^2d+3abc^2+6abcd+3abd^2+2ac^3+6ac^2d+6acd^2+2ad^3+b^2c^2+2b^2cd+b^2d^2+2bc^3+6bc^2d+6bcd^2+2bd^3+c^4+4c^3d+6c^2d^2+4cd^3+d^4$$\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",
"$$ abc^2 \\le \n",
"a^3c+a^3d+a^2b^2+a^2bd+a^2c^2+2a^2cd+a^2d^2+ab^3+ab^2c+2ab^2d+abd^2+b^3c+b^3d+b^2c^2+2b^2cd+b^2d^2 $$\n"
]
},
{
"data": {
"text/plain": [
"0"
]
},
"execution_count": 16,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"prove(makesubs(formula,'[c,inf],[d,inf]'))"
]
},
{
"cell_type": "code",
"execution_count": 17,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Substitute $ a \\to a+c $\n",
"Substitute $ b \\to b+d $\n",
"numerator: $$2a^3c+2a^3d+2a^2b^2+2a^2bd+2a^2c^2+4a^2cd+2a^2d^2+2ab^3+2ab^2c+4ab^2d-2abc^2+2abd^2+2b^3c+2b^3d+2b^2c^2+4b^2cd+2b^2d^2$$\n",
"denominator: $$a^2bc+a^2bd+a^2c^2+2a^2cd+a^2d^2+ab^2c+ab^2d+3abc^2+6abcd+3abd^2+2ac^3+6ac^2d+6acd^2+2ad^3+b^2c^2+2b^2cd+b^2d^2+2bc^3+6bc^2d+6bcd^2+2bd^3+c^4+4c^3d+6c^2d^2+4cd^3+d^4$$\n",
"status: 0\n",
"From weighted AM-GM inequality:\n",
"$$2abc^2 \\le a^2c^2+b^2c^2$$\n",
"\n",
"$$ 0 \\le \n",
"2a^3c+2a^3d+2a^2b^2+2a^2bd+a^2c^2+4a^2cd+2a^2d^2+2ab^3+2ab^2c+4ab^2d+2abd^2+2b^3c+2b^3d+b^2c^2+4b^2cd+2b^2d^2 $$\n",
"The sum of all inequalities gives us a proof of the inequality.\n"
]
},
{
"data": {
"text/plain": [
"0"
]
},
"execution_count": 17,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"prove(makesubs(formula,'[c,inf],[d,inf]')*2)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"It's a good idea to use intervals that are unbounded from one side (i.e. those which contain $\\pm\\infty$). In this problem we could assume that $a\\in (0,c]$, $b\\in (0,d]$ as well. But as you can see, in this case the proof is several times longer."
]
},
{
"cell_type": "code",
"execution_count": 18,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Substitute $ a \\to c-c/(a+1) $\n",
"Substitute $ b \\to d-d/(b+1) $\n",
"numerator: $$2a^3bc^2d^2+4a^3bcd^3+2a^3bd^4+2a^3c^2d^2+2a^3cd^3-2a^2b^2c^3d+2a^2b^2cd^3-4a^2bc^3d+4a^2bc^2d^2+12a^2bcd^3+6a^2bd^4-2a^2c^3d+4a^2c^2d^2+6a^2cd^3+2ab^3c^4+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+2ac^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",
"denominator: $$a^3b^3c^4+4a^3b^3c^3d+6a^3b^3c^2d^2+4a^3b^3cd^3+a^3b^3d^4+3a^3b^2c^4+10a^3b^2c^3d+12a^3b^2c^2d^2+6a^3b^2cd^3+a^3b^2d^4+3a^3bc^4+8a^3bc^3d+7a^3bc^2d^2+2a^3bcd^3+a^3c^4+2a^3c^3d+a^3c^2d^2+a^2b^3c^4+6a^2b^3c^3d+12a^2b^3c^2d^2+10a^2b^3cd^3+3a^2b^3d^4+3a^2b^2c^4+15a^2b^2c^3d+24a^2b^2c^2d^2+15a^2b^2cd^3+3a^2b^2d^4+3a^2bc^4+12a^2bc^3d+14a^2bc^2d^2+5a^2bcd^3+a^2c^4+3a^2c^3d+2a^2c^2d^2+2ab^3c^3d+7ab^3c^2d^2+8ab^3cd^3+3ab^3d^4+5ab^2c^3d+14ab^2c^2d^2+12ab^2cd^3+3ab^2d^4+4abc^3d+8abc^2d^2+4abcd^3+ac^3d+ac^2d^2+b^3c^2d^2+2b^3cd^3+b^3d^4+2b^2c^2d^2+3b^2cd^3+b^2d^4+bc^2d^2+bcd^3$$\n",
"status: 0\n",
"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",
"\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",
"The sum of all inequalities gives us a proof of the inequality.\n"
]
},
{
"data": {
"text/plain": [
"0"
]
},
"execution_count": 18,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"prove(makesubs(formula,'[0,c],[0,d]')*2)"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
"kernelspec": {
"display_name": "SageMath 9.0",
"language": "sage",
"name": "sagemath"
},
"language_info": {
"codemirror_mode": {
"name": "ipython",
"version": 3
},
"file_extension": ".py",
"mimetype": "text/x-python",
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.7.3"
}
},
"nbformat": 4,
"nbformat_minor": 2
}

BIN
__pycache__/shiroindev.cpython-37.pyc Normal file
View File

Binary file not shown.

824
examples.ipynb Normal file
View File

@ -0,0 +1,824 @@
{
"cells": [
{
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [
{
"name": "stderr",
"output_type": "stream",
"text": [
"/home/grzegorz/shiroindev/shiroindev.py:40: DeprecationWarning: invalid escape sequence \\^\n",
" formula=re.sub('\\^{(.)}',r'^\\1',latex(formula,fold_short_frac=True).replace(' ','').replace('\\\\left(','(').replace('\\\\right)',')'))\n",
"/home/grzegorz/shiroindev/shiroindev.py:41: DeprecationWarning: invalid escape sequence \\{\n",
" return re.sub('\\{(\\(.+?\\))\\}',r'\\1',formula)\n"
]
}
],
"source": [
"from shiroindev import *\n",
"sSeed=1"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The first line obviously loads this package. The second one sets a seed for proving functions. If you don't write it, you can get slightly different proof each time you run a function. \n",
"\n",
"Now let's make some proofs. We will use problems from https://www.imomath.com/index.php?options=593&lmm=0."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Problem 1\n",
"Prove the inequality $a^2+b^2+c^2\\ge ab+bc+ca$, if $a,b,c$ are real numbers."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Function `prove` tries to prove that given formula is nonnegative, **assuming all variables are nonnegative**. In this case the nonnegativity assumption is not a problem, since all powers on the left side are even, so if $|a|^2+|b|^2+|c|^2 \\ge |ab|+|ac|+|bc|,$ then $a^2+b^2+c^2= |a|^2+|b|^2+|c|^2 \\ge |ab|+|ac|+|bc| \\ge ab+ac+bc$."
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"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"
]
},
{
"data": {
"text/plain": [
"0"
]
},
"execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"prove('(a^2+b^2+c^2-a*b-a*c-b*c)')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Function prove prints several things. The first two gives us a formula after expanding it. To proceed, a **numerator** has to be a **polynomial with integer coefficients**. The next one is status, which is the return status of the first use of ```scipy.optimize.linprog```. Possible outputs and explanations are\n",
"\n",
"* 0 - found a proof with real coefficients,\n",
"* 1 - need more time, \n",
"* 2 - function didn't find a proof,\n",
"* 3,4 - loss of precision (which may happen if it has to work with big numbers).\n",
"\n",
"Then we've got a hint. So let's use it!"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"numerator: $$2a^2-2ab-2ac+2b^2-2bc+2c^2$$\n",
"denominator: $$1$$\n",
"status: 0\n",
"From weighted AM-GM inequality:\n",
"$$2ab \\le a^2+b^2$$\n",
"$$2ac \\le a^2+c^2$$\n",
"$$2bc \\le b^2+c^2$$\n",
"\n",
"$$ 0 \\le \n",
"0 $$\n",
"The sum of all inequalities gives us a proof of the inequality.\n"
]
},
{
"data": {
"text/plain": [
"0"
]
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"prove('(a^2+b^2+c^2-a*b-a*c-b*c)*2')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Problem 2\n",
"Find all real numbers such that $a^2+b^2+c^2+d^2=a(b+c+d)$. "
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"At first glance it doesn't look like an inequality problem, but actually it is one. If you try to calculate both sides for different values, you can see that the left side of the equation is never less than the right one. So let's try"
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"numerator: $$a^2-ab-ac-ad+b^2+c^2+d^2$$\n",
"denominator: $$1$$\n",
"status: 2\n",
"\n",
"Program couldn't find any proof.\n",
"$$ ab+ac+ad \\le \n",
"a^2+b^2+c^2+d^2 $$\n"
]
},
{
"data": {
"text/plain": [
"2"
]
},
"execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"prove('a^2+b^2+c^2+d^2-a*(b+c+d)')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"This time `prove` didn't found the proof. But it doesn't mean that the inequality is not true! `prove` uses a list of values for which the formula should be small. There is no strict rule here, but the smaller that value is, the higher are chances to find a proof. List of values should correspond to the list of variables in alphabetical order. So let's try $a=2$ and $b=c=d=1$."
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Substitute $ a \\to 2a $\n",
"numerator: $$4a^2-2ab-2ac-2ad+b^2+c^2+d^2$$\n",
"denominator: $$1$$\n",
"status: 0\n",
"From weighted AM-GM inequality:\n",
"$$2ab \\le a^2+b^2$$\n",
"$$2ac \\le a^2+c^2$$\n",
"$$2ad \\le a^2+d^2$$\n",
"\n",
"$$ 0 \\le \n",
"a^2 $$\n",
"The sum of all inequalities gives us a proof of the inequality.\n"
]
},
{
"data": {
"text/plain": [
"0"
]
},
"execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"prove('a^2+b^2+c^2+d^2-a*(b+c+d)','2,1,1,1')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Function makes a substitution $a\\to 2a$ (which should be understood as $a=2a'$) and try to prove new inequality. This time it succeeded. Moreover, if starting formula is equal to 0, then all these inequalities have to be equalities, so $a'^2=0$ and eventually $a=0$. We can also try a little bit lower value for $a$."
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Substitute $ a \\to 7a/4 $\n",
"numerator: $$49a^2-28ab-28ac-28ad+16b^2+16c^2+16d^2$$\n",
"denominator: $$16$$\n",
"status: 0\n",
"From weighted AM-GM inequality:\n",
"$$28ab \\le 14a^2+14b^2$$\n",
"$$28ac \\le 14a^2+14c^2$$\n",
"$$28ad \\le 14a^2+14d^2$$\n",
"\n",
"$$ 0 \\le \n",
"7a^2+2b^2+2c^2+2d^2 $$\n",
"The sum of all inequalities gives us a proof of the inequality.\n"
]
},
{
"data": {
"text/plain": [
"0"
]
},
"execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"prove('a^2+b^2+c^2+d^2-a*(b+c+d)','7/4,1,1,1')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Now we can see that if $a^2+b^2+c^2+d^2-a(b+c+d)=0$, then $7a'^2+2b^2+2c^2+2d^2=0$ and eventually $a=b=c=d=0$. Note that inequality is proved only for positive numbers (which, by continuity, can be expanded to nonnegative numbers). But using similar argumentation to the one in previous problem, if $(a,b,c,d)=(x,y,z,t)$ is the solution of $a^2+b^2+c^2+d^2-a(b+c+d)=0$, then $(a,b,c,d)=(|x|,|y|,|z|,|t|)$ is a solution, too. Since the only nonnegative solution is $(0,0,0,0)$, it means that it is the only solution.\n",
"\n",
"Let's skip the problem 3 and look solve the problem 4 instead.\n",
"\n",
"#### Problem 4\n",
"If $x$ and $y$ are two positive numbers less than 1, prove that\n",
"$$\\frac{1}{1-x^2}+\\frac{1}{1-y^2}\\ge \\frac{2}{1-xy}.$$"
]
},
{
"cell_type": "code",
"execution_count": 7,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"numerator: $$-x^3y+2x^2y^2-x^2-xy^3+2xy-y^2$$\n",
"denominator: $$x^3y^3-x^3y-x^2y^2+x^2-xy^3+xy+y^2-1$$\n",
"status: 2\n",
"\n",
"Program couldn't find any proof.\n",
"$$ x^3y+x^2+xy^3+y^2 \\le \n",
"2x^2y^2+2xy $$\n",
"It looks like the formula is symmetric. You can assume without loss of generality that x >= y Try\n",
"prove(makesubs(S(\" -x**3*y + 2*x**2*y**2 - x**2 - x*y**3 + 2*x*y - y**2 \"), [('y', 'inf')] )\n"
]
},
{
"data": {
"text/plain": [
"2"
]
},
"execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"prove('1/(1-x^2)+1/(1-y^2)-2/(1-x*y)')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"`prove` assumes that formula is well-defined if all variables are positive, so it doesn't have to analyze the denominator (except of choosing the right sign). In this case it is not true, since if $x=1$, then $1-x^2=0$. Also denominator is equal to $(x^2-1)(y^2-1)(xy-1)$ which is negative for $x,y\\in (0,1)$. So we need to make some substitution after which new variables can have all positive values, not just these inside (0,1) interval.\n",
"\n",
"We will use a function `makesubs` to generate these substitutions. It has three basic parameters: `formula`, `intervals` and `values`. `intervals` are current limitations of variables, `values` are values of variables for which `formula` is small. `values` should be inside corresponding `intervals`. This argument is optional but it's better to use it.\n",
"Let's go back to our problem. If $x=y$, then $\\frac{1}{1-x^2}+\\frac{1}{1-y^2}\\ge \\frac{2}{1-xy}$, so it's the minimum value of the formula. So let `values=(1/2,1/2)` (**warning: do not use decimal point**, for example '0.5,0.5')."
]
},
{
"cell_type": "code",
"execution_count": 8,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Substitute $ x \\to 1-1/(x+1) $\n",
"Substitute $ y \\to 1-1/(y+1) $\n",
"numerator: $$6x^3y+3x^3-12x^2y^2-3x^2y+3x^2+6xy^3-3xy^2-6xy+3y^3+3y^2$$\n",
"denominator: $$4x^2y+2x^2+4xy^2+8xy+3x+2y^2+3y+1$$\n",
"status: 0\n",
"From weighted AM-GM inequality:\n",
"$$12x^2y^2 \\le 6x^3y+6xy^3$$\n",
"$$3x^2y \\le 2x^3+y^3$$\n",
"$$3xy^2 \\le x^3+2y^3$$\n",
"$$6xy \\le 3x^2+3y^2$$\n",
"\n",
"$$ 0 \\le \n",
"0 $$\n",
"The sum of all inequalities gives us a proof of the inequality.\n"
]
},
{
"data": {
"text/plain": [
"0"
]
},
"execution_count": 8,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"newformula,newvalues=makesubs('1/(1-x^2)+1/(1-y^2)-2/(1-x*y)','[0,1],[0,1]','1/2,1/2')\n",
"prove(newformula*3,newvalues)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Now let's get back to problem 3.\n",
"\n",
"#### Problem 3\n",
"\n",
"If $a,b,c$ are positive real numbers that satisfy $a^2+b^2+c^2=1$, find the minimal value of\n",
"$$\\frac{a^2b^2}{c^2}+\\frac{b^2c^2}{a^2}+\\frac{c^2a^2}{b^2}$$\n",
"\n",
"The problem is equivalent to finding minimum of $xy/z+yz/x+zx/y$ assuming $x+y+z=1$ and $x,y,z>0$. The first idea is to suppose that the minimum is reached when $x=y=z$. In that case, $x=y=z=1/3$ and formula is equal to 1. Now we can substitute $z\\to 1-x-y$. Constraints for variables are $x>0$, $y>0$, $x+y<1$. We can rewrite it as $x \\in (0,1-y)$, $y \\in (0,1)$. These two conditions have two important properties:\n",
"* constraints for variables are written as intervals,\n",
"* there are no \"backwards dependencies\", i.e. there is no $x$ in the interval of $y$.\n",
"\n",
"If these two conditions hold, then you can use `makesubs` function.\n",
"**Warning:** at this moment `makesubs` **doesn't warn you if your list of intervals doesn't follow these rules!**\n"
]
},
{
"cell_type": "code",
"execution_count": 9,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Substitute $ x \\to -y+1+(y-1)/(x+1) $\n",
"Substitute $ y \\to 1-1/(y+1) $\n",
"Substitute $ y \\to y/2 $\n",
"numerator: $$x^4y^2+x^3y^2-2x^3y-4x^2y+4x^2+xy^2-2xy+y^2$$\n",
"denominator: $$x^3y^2+2x^3y+2x^2y^2+4x^2y+xy^2+2xy$$\n",
"status: 0\n",
"From weighted AM-GM inequality:\n",
"$$2x^3y \\le x^4y^2+x^2$$\n",
"$$4x^2y \\le x^3y^2+2x^2+xy^2$$\n",
"$$2xy \\le x^2+y^2$$\n",
"\n",
"$$ 0 \\le \n",
"0 $$\n",
"The sum of all inequalities gives us a proof of the inequality.\n"
]
},
{
"data": {
"text/plain": [
"0"
]
},
"execution_count": 9,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"formula=Sm('xy/z+yz/x+zx/y-1').subs('z',S('1-x-y'))\n",
"newformula,values=makesubs(formula,'[0,1-y],[0,1]','1/3,1/3')\n",
"prove(newformula,values)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The proof is found, so the assumption that 1 is the minimum of `xy/z+yz/x+zx/y` was good.\n",
"\n",
"Functions `S` and `Sm` creates a SymPy object from a string. The only difference is that `Sm` assumes that there are no multi-letter variables and adds a multiplication sign between every two terms which has no operator sign, so object `Sm(xy/z+yz/x+zx/y)` has 3 variables `x,y,z` and `S('xy/z+yz/x+zx/y')` has 6 variables `x,y,z,xy,yz,zx`. \n",
"\n",
"As you may have noticed, formulas are often cyclic or symmetric. Therefore you can use `cyclize` or `symmetrize` function to reduce the length of the written formula. Here are a few commands which will do the same as each other. "
]
},
{
"cell_type": "code",
"execution_count": 10,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"numerator: $$2a^2-2ab-2ac+2b^2-2bc+2c^2$$\n",
"denominator: $$1$$\n",
"status: 0\n",
"From weighted AM-GM inequality:\n",
"$$2ab \\le a^2+b^2$$\n",
"$$2ac \\le a^2+c^2$$\n",
"$$2bc \\le b^2+c^2$$\n",
"\n",
"$$ 0 \\le \n",
"0 $$\n",
"The sum of all inequalities gives us a proof of the inequality.\n"
]
},
{
"data": {
"text/plain": [
"0"
]
},
"execution_count": 10,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"prove('(a^2+b^2+c^2-a*b-a*c-b*c)*2')\n",
"#prove(S('(a^2+b^2+c^2-a*b-a*c-b*c)*2'))\n",
"#prove(Sm('2(a^2+b^2+c^2-ab-ac-bc)'))\n",
"#prove(cyclize('2*a^2-2*a*b'))\n",
"#prove(symmetrize('a^2-a*b'))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Now look at formula $(x-1)^4$. It's quite obvious that it's nonnegative, but `prove` fails to show this!"
]
},
{
"cell_type": "code",
"execution_count": 11,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"numerator: $$x^4-4x^3+6x^2-4x+1$$\n",
"denominator: $$1$$\n",
"status: 2\n",
"\n",
"Program couldn't find any proof.\n",
"$$ 4x^3+4x \\le \n",
"x^4+6x^2+1 $$\n"
]
},
{
"data": {
"text/plain": [
"2"
]
},
"execution_count": 11,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"prove('(x-1)^4')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"But there is a relatively simple method to generate a proof using this library. We will make to proofs: one for $x\\in (1,\\infty)$ and the second one for $(-\\infty,1)$."
]
},
{
"cell_type": "code",
"execution_count": 12,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Substitute $ x \\to x+1 $\n",
"numerator: $$x^4$$\n",
"denominator: $$1$$\n",
"status: 0\n",
"\n",
"$$ 0 \\le \n",
"x^4 $$\n",
"The sum of all inequalities gives us a proof of the inequality.\n"
]
},
{
"data": {
"text/plain": [
"0"
]
},
"execution_count": 12,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"prove(makesubs('(x-1)^4','(1,inf)'))"
]
},
{
"cell_type": "code",
"execution_count": 13,
"metadata": {
"scrolled": true
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Substitute $ x \\to 1-x $\n",
"numerator: $$x^4$$\n",
"denominator: $$1$$\n",
"status: 0\n",
"\n",
"$$ 0 \\le \n",
"x^4 $$\n",
"The sum of all inequalities gives us a proof of the inequality.\n"
]
},
{
"data": {
"text/plain": [
"0"
]
},
"execution_count": 13,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"prove(makesubs('(x-1)^4','(-inf,1)'))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Now let's go to the problem 10\n",
"#### Problem 10\n",
"If $a,b,c,d>0$, prove that\n",
"$$\\frac a{b+c}+\\frac b{c+d}+ \\frac c{d+a}+ \\frac d{a+b}\\geq 2.$$\n",
"\n",
"Let's try a simple approach."
]
},
{
"cell_type": "code",
"execution_count": 14,
"metadata": {},
"outputs": [
{
"data": {
"text/latex": [
"$\\displaystyle \\frac{a}{b + c} + \\frac{b}{c + d} + \\frac{c}{a + d} + \\frac{d}{a + b} - 2$"
],
"text/plain": [
"a/(b + c) + b/(c + d) + c/(a + d) + d/(a + b) - 2"
]
},
"execution_count": 14,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"formula=cyclize('a/(b+c)',variables='a,b,c,d')-2\n",
"formula"
]
},
{
"cell_type": "code",
"execution_count": 15,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"numerator: $$a^3c+a^3d+a^2b^2-a^2bd-2a^2c^2-a^2cd+a^2d^2+ab^3-ab^2c-ab^2d-abc^2+ac^3-acd^2+b^3d+b^2c^2-2b^2d^2+bc^3-bc^2d-bcd^2+bd^3+c^2d^2+cd^3$$\n",
"denominator: $$a^2bc+a^2bd+a^2c^2+a^2cd+ab^2c+ab^2d+abc^2+2abcd+abd^2+ac^2d+acd^2+b^2cd+b^2d^2+bc^2d+bcd^2$$\n",
"status: 2\n",
"\n",
"Program couldn't find any proof.\n",
"$$ a^2bd+2a^2c^2+a^2cd+ab^2c+ab^2d+abc^2+acd^2+2b^2d^2+bc^2d+bcd^2 \\le \n",
"a^3c+a^3d+a^2b^2+a^2d^2+ab^3+ac^3+b^3d+b^2c^2+bc^3+bd^3+c^2d^2+cd^3 $$\n"
]
},
{
"data": {
"text/plain": [
"2"
]
},
"execution_count": 15,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"prove(formula)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"This problem, like the previous one, can be solved by splitting the domain of variables to several subdomains. But we can also use the symmetry of this inequality. For example, without loss of generality we can assume that $a\\ge c$ and $b\\ge d$, so $a\\in [c,\\infty)$, $b\\in [d,\\infty)$."
]
},
{
"cell_type": "code",
"execution_count": 16,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Substitute $ a \\to a+c $\n",
"Substitute $ b \\to b+d $\n",
"numerator: $$a^3c+a^3d+a^2b^2+a^2bd+a^2c^2+2a^2cd+a^2d^2+ab^3+ab^2c+2ab^2d-abc^2+abd^2+b^3c+b^3d+b^2c^2+2b^2cd+b^2d^2$$\n",
"denominator: $$a^2bc+a^2bd+a^2c^2+2a^2cd+a^2d^2+ab^2c+ab^2d+3abc^2+6abcd+3abd^2+2ac^3+6ac^2d+6acd^2+2ad^3+b^2c^2+2b^2cd+b^2d^2+2bc^3+6bc^2d+6bcd^2+2bd^3+c^4+4c^3d+6c^2d^2+4cd^3+d^4$$\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",
"$$ abc^2 \\le \n",
"a^3c+a^3d+a^2b^2+a^2bd+a^2c^2+2a^2cd+a^2d^2+ab^3+ab^2c+2ab^2d+abd^2+b^3c+b^3d+b^2c^2+2b^2cd+b^2d^2 $$\n"
]
},
{
"data": {
"text/plain": [
"0"
]
},
"execution_count": 16,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"prove(makesubs(formula,'[c,inf],[d,inf]'))"
]
},
{
"cell_type": "code",
"execution_count": 17,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Substitute $ a \\to a+c $\n",
"Substitute $ b \\to b+d $\n",
"numerator: $$2a^3c+2a^3d+2a^2b^2+2a^2bd+2a^2c^2+4a^2cd+2a^2d^2+2ab^3+2ab^2c+4ab^2d-2abc^2+2abd^2+2b^3c+2b^3d+2b^2c^2+4b^2cd+2b^2d^2$$\n",
"denominator: $$a^2bc+a^2bd+a^2c^2+2a^2cd+a^2d^2+ab^2c+ab^2d+3abc^2+6abcd+3abd^2+2ac^3+6ac^2d+6acd^2+2ad^3+b^2c^2+2b^2cd+b^2d^2+2bc^3+6bc^2d+6bcd^2+2bd^3+c^4+4c^3d+6c^2d^2+4cd^3+d^4$$\n",
"status: 0\n",
"From weighted AM-GM inequality:\n",
"$$2abc^2 \\le a^2c^2+b^2c^2$$\n",
"\n",
"$$ 0 \\le \n",
"2a^3c+2a^3d+2a^2b^2+2a^2bd+a^2c^2+4a^2cd+2a^2d^2+2ab^3+2ab^2c+4ab^2d+2abd^2+2b^3c+2b^3d+b^2c^2+4b^2cd+2b^2d^2 $$\n",
"The sum of all inequalities gives us a proof of the inequality.\n"
]
},
{
"data": {
"text/plain": [
"0"
]
},
"execution_count": 17,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"prove(makesubs(formula,'[c,inf],[d,inf]')*2)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"It's a good idea to use intervals that are unbounded from one side (i.e. those which contain $\\pm\\infty$). In this problem we could assume that $a\\in (0,c]$, $b\\in (0,d]$ as well. But as you can see, in this case the proof is several times longer."
]
},
{
"cell_type": "code",
"execution_count": 18,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Substitute $ a \\to c-c/(a+1) $\n",
"Substitute $ b \\to d-d/(b+1) $\n",
"numerator: $$2a^3bc^2d^2+4a^3bcd^3+2a^3bd^4+2a^3c^2d^2+2a^3cd^3-2a^2b^2c^3d+2a^2b^2cd^3-4a^2bc^3d+4a^2bc^2d^2+12a^2bcd^3+6a^2bd^4-2a^2c^3d+4a^2c^2d^2+6a^2cd^3+2ab^3c^4+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+2ac^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",
"denominator: $$a^3b^3c^4+4a^3b^3c^3d+6a^3b^3c^2d^2+4a^3b^3cd^3+a^3b^3d^4+3a^3b^2c^4+10a^3b^2c^3d+12a^3b^2c^2d^2+6a^3b^2cd^3+a^3b^2d^4+3a^3bc^4+8a^3bc^3d+7a^3bc^2d^2+2a^3bcd^3+a^3c^4+2a^3c^3d+a^3c^2d^2+a^2b^3c^4+6a^2b^3c^3d+12a^2b^3c^2d^2+10a^2b^3cd^3+3a^2b^3d^4+3a^2b^2c^4+15a^2b^2c^3d+24a^2b^2c^2d^2+15a^2b^2cd^3+3a^2b^2d^4+3a^2bc^4+12a^2bc^3d+14a^2bc^2d^2+5a^2bcd^3+a^2c^4+3a^2c^3d+2a^2c^2d^2+2ab^3c^3d+7ab^3c^2d^2+8ab^3cd^3+3ab^3d^4+5ab^2c^3d+14ab^2c^2d^2+12ab^2cd^3+3ab^2d^4+4abc^3d+8abc^2d^2+4abcd^3+ac^3d+ac^2d^2+b^3c^2d^2+2b^3cd^3+b^3d^4+2b^2c^2d^2+3b^2cd^3+b^2d^4+bc^2d^2+bcd^3$$\n",
"status: 0\n",
"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",
"\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",
"The sum of all inequalities gives us a proof of the inequality.\n"
]
},
{
"data": {
"text/plain": [
"0"
]
},
"execution_count": 18,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"prove(makesubs(formula,'[0,c],[0,d]')*2)"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
"kernelspec": {
"display_name": "SageMath 9.0",
"language": "sage",
"name": "sagemath"
},
"language_info": {
"codemirror_mode": {
"name": "ipython",
"version": 3
},
"file_extension": ".py",
"mimetype": "text/x-python",
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.7.3"
}
},
"nbformat": 4,
"nbformat_minor": 2
}

442
shiroindev.py Normal file
View File

@ -0,0 +1,442 @@
from __future__ import print_function
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={}
translationList=['numerator:','denominator:','status:',
'Substitute',"Formula after substitution:",
"Numerator after substitutions:","From weighted AM-GM inequality:",
'The sum of all inequalities gives us a proof of the inequality.',
"Program couldn't find a solution with integer coefficients. Try "+
"to multiple the formula by some integer and run this function again.",
"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"
]
#Initialize english-english dictionary.
for phrase in translationList:
sTranslation[phrase]=phrase
from scipy.optimize import linprog
import random
from sympy import S,cancel,fraction,Pow,expand,solve,latex
import re
def _remzero(coef,fun):
#coef, fun represents an expression.
#For example, if expression=5f(2,3)+0f(4,6)+8f(1,4)
#then coef=[5,0,8], fun=[[2,3],[4,6],[1,4]]
#_remzero removes addends with coefficient equal to zero.
#In this example ncoef=[5,8], nfun=[[2,3],[1,4]]
ncoef=[]
nfun=[]
for c,f in zip(coef,fun):
if c>0:
ncoef+=[c]
nfun+=[f]
return ncoef,nfun
def slatex(formula): #fancy function which makes latex code more readable, but still correct
formula=re.sub('\^{(.)}',r'^\1',latex(formula,fold_short_frac=True).replace(' ','').replace('\\left(','(').replace('\\right)',')'))
return re.sub('\{(\(.+?\))\}',r'\1',formula)
def _writ2(coef,fun,variables):
return slatex(S((str(coef)+'*'+'*'.join([str(x)+'^'+str(y) for x,y in zip(variables,fun)]))))
def _writ(coef,fun,nullvar):
return str(coef)+'f('+str(fun)[1:-1-(len(fun)==1)]+')'
def _check(coef,fun,res,rfun):
#checks if rounding and all the floating point stuff works
res2=[int(round(x)) for x in res]
b1=[coef*x for x in fun]
b2=[[x*y for y in rfuni] for x,rfuni in zip(res2,rfun)]
return b1==[sum(x) for x in zip(*b2)] and coef==sum(res2)
def _powr(formula):
if formula.func==Pow:
return formula.args
else:
return [formula,S('1')]
def fractioncancel(formula):
#workaround for buggy cancel function
num,den=fraction(cancel(formula/S('tmp')))
den=den.subs('tmp','1')
return num,den
def ssolve(formula,variables):
#workaround for inconsistent solve function
result=solve(formula,variables)
if type(result)==dict:
result=[[result[var] for var in variables]]
return result
def sstr(formula):
return str(formula).replace('**','^').replace('*','').replace(' ','')
def Sm(formula):
#Adds multiplication signs and sympifies a formula.
#For example, Sm('(2x+y)(7+5xz)') -> S('(2*x+y)*(7+5*x*z)')
if type(formula)==str:
formula.replace(' ','')
for i in range(2):
formula=re.sub(r'([0-9a-zA-Z)])([(a-zA-Z])',r'\1*\2',formula)
formula=S(formula)
return formula
def _input2fraction(formula,variables,values):
#makes some substitutions and converts formula to a fraction
#with expanded numerator and denominator
formula=S(formula)
subst=[]
for x,y in zip(variables,values):
if y!=1:
print(sTranslation['Substitute'],'$',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)+'$$')
return (numerator,denominator)
def _formula2list(formula,variables):
#Splits a polynomial to a difference of two polynomials with positive
#coefficients and extracts coefficients and powers of both polynomials.
#'variables' is used to set order of powers
#For example, If formula=5x^2-4xy+8y^3, variables=[x,y], then
#the program tries to prove that
#0<=5x^2-4xy+8y^3
#4xy<=5x^2+8y^3
#lcoef=[4]
#lfun=[[1,1]]
#rcoef=[5,8]
#rfun=[[2,0],[0,3]]
lfun=[]
lcoef=[]
rfun=[]
rcoef=[]
varorder=dict(zip(variables,range(len(variables))))
for addend in formula.as_ordered_terms():
coef,facts=addend.as_coeff_mul()
powers=[0]*len(variables)
for var in variables:
powers[varorder[var]]=0
for fact in facts:
var,pw=_powr(fact)
powers[varorder[var]]=int(pw)
if(coef<0):
lcoef+=[-coef]
lfun+=[powers]
else:
rcoef+=[coef]
rfun+=[powers]
return(lcoef,lfun,rcoef,rfun)
def _list2proof(lcoef,lfun,rcoef,rfun,variables,itermax,linprogiter,_writ2=_writ2):
#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).
#suppose we are trying to prove that
#30x^2y^2+60xy^4<=48x^3+56y^6 (assuming x,y>0)
#program will try to find some a,b,c,d such that
#30x^2y^2<=ax^3+by^6
#60xy^4<=cx^3+dy^6
#where a+c<=48 and b+d<=56 (assumption 1)
#We need some additional equalities to meet assumptions
#of the weighted AM-GM inequality.
#a+b=30 and c+d=60 (assumption 2)
#3a+0b=30*2, 0a+6b=30*2, 3c+0d=60*1, 0c+6d=60*4 (assumption 3)
#The sketch of the algorithm.
# for i in range(itermax):
#1. Create a vector of random numbers (weights).
#2. Try to find real solution of the problem (with linprog).
#3. If there is no solution (status: 2)
#3a. If the solution was never found, break.
#3b. Else, step back (to the bigger inequality)
#4. If the soltuion was found (status: 0)
#Check out which of variables (in example: a,b,c,d) looks like integer.
#If there are some inequalities with all integer coefficients, subtract
#them from the original one.
#If LHS is empty, then break.
localseed=sSeed
bufer=''
itern=0
if len(lcoef)==0: #if LHS is empty
print(sTranslation['status:'], 0)
status=0
elif len(rcoef)==0:
#if RHS is empty, but LHS is not
print(sTranslation['status:'], 2)
status=2
itermax=0
foundreal=0
while len(lcoef)>0 and itern<itermax:
itern+=1
m=len(lcoef)
n=len(rcoef)
#lfunt=transposed matrix lfun (in fact, it's
#a list of lists)
lfunt=list(map(list, zip(*lfun)))
rfunt=list(map(list, zip(*rfun)))
#A,b, - set of linear equalities
#A_ub,b_ub - set of linear inequalities
#from linear program
A=[]
b=[]
A_ub=[]
b_ub=[]
for i in range(m):
for j in range(len(rfunt)): #assumption 3
A+=[[0]*(m*n)]
A[-1][i*n:i*n+n]=rfunt[j]
b+=[lfun[i][j]*lcoef[i]]
A+=[[0]*(m*n)] #assumption 2
A[-1][i*n:i*n+n]=[1]*n
b+=[lcoef[i]]
for j in range(n): #assumption 1
A_ub+=[[0]*(m*n)]
A_ub[-1][j::n]=[1]*m
b_ub+=[rcoef[j]]
random.seed(localseed)
vecc=[random.random() for i in range(m*n)]
localseed=random.randint(1,1000000000)
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)
if status==0:
print(sTranslation['From weighted AM-GM inequality:'])
if status==2: #if real solution of current inequality doesn't exist
if foundreal==0: #if this is the first inequality, then break
break
else:
#step back
lcoef,lfun=oldlcoef,oldlfun
rcoef,rfun=oldrcoef,oldrfun
bufer=''
continue
if status==0:#if found a solution with real coefficients
print(bufer,end='')
foundreal=1
bufer=''
oldlfun,oldrfun=lfun,rfun
oldlcoef,oldrcoef=lcoef[:],rcoef[:]
for i in range(m):
c=0
for j in res.x[i*n:i*n+n]:#check if all coefficients
#in an equality looks like integers
if(abs(round(j)-j)>0.0001):
break
else:
#checks if rounding all coefficients doesn't make
#inequality false
isok=_check(lcoef[i],lfun[i],res.x[i*n:i*n+n],rfun)
if not isok:
continue
bufer+='$$'+_writ2(lcoef[i],lfun[i],variables)+' \\le '
lcoef[i]=0
for j in range(n):
rcoef[j]-=int(round(res.x[i*n+j]))
for j,k in zip(res.x[i*n:i*n+n],rfun):
if j<0.0001:
continue
if(c):bufer+='+'
else:c=1
bufer+=_writ2(int(round(j)),k,variables)
bufer+='$$\n'
lcoef,lfun=_remzero(lcoef,lfun)
rcoef,rfun=_remzero(rcoef,rfun)
print(bufer)
lhs='+'.join([_writ2(c,f,variables) for c,f in zip(lcoef,lfun)])
if lhs=='':
lhs='0'
elif status==0:
print(sTranslation[
"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."])
#return res.status
elif status==1:
print(sTranslation["Try to set higher linprogiter parameter."])
print('$$ ',slatex(lhs),' \\le ')
rhs='+'.join([_writ2(c,f,variables) for c,f in zip(rcoef,rfun)])
if rhs=='':
rhs='0'
print(slatex(rhs),' $$')
if lhs=='0':
print(sTranslation['The sum of all inequalities gives us a proof of the inequality.'])
return status
def _isiterable(obj):
try:
_ = (e for e in obj)
return True
except TypeError:
return False
def _smakeiterable(x):
x=S(x)
if _isiterable(x):
return x
return (x,)
def _smakeiterable2(x):
x=S(x)
if _isiterable(x[0]):
return x
return (x,)
def prove(formula,values=None,variables=None,niter=200,linprogiter=10000):
#tries to prove that formula>=0 assuming all variables are positive
formula=S(formula)
if variables: variables=_smakeiterable(variables)
else: variables=sorted(formula.free_symbols,key=str)
if values: values=_smakeiterable(values)
else: values=[1]*len(variables)
num,den=_input2fraction(formula,variables,values)
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:]],')')
return st
def powerprove(formula,values=None,variables=None,niter=200,linprogiter=10000):
#This is a bruteforce and ineffective function for proving inequalities.
#It can be used as the last resort.
formula=S(formula)
if variables: variables=_smakeiterable(variables)
else: variables=sorted(formula.free_symbols,key=str)
if values: values=_smakeiterable(values)
else: values=[1]*len(variables)
num,den=_input2fraction(formula,variables,values)
subst2=[]
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')
subst1=[]
substout=[]
for j in range(len(variables)):
if i&(1<<j):
subst1+=[(variables[j],1/variables[j])]
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)+'$')
num1=fractioncancel(num.subs(subst1))[0]
num2=expand(num1.subs(subst2))
print(sTranslation["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:
#for all positive variables new formula is nonnegative iff
#for all variables in corresponding intervals old formula is nonnegative
formula=S(formula)
intervals=_smakeiterable2(intervals)
if variables: variables=_smakeiterable(variables)
else: variables=sorted(formula.free_symbols,key=str)
if values!=None:
values=_smakeiterable(values)
equations=[var-value for var,value in zip(variables,values)]
else:
equations=[]
for var,interval in zip(variables,intervals):
end1,end2=interval
if end1 in {S('-inf'),S('inf')}:
end1,end2=end2,end1
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,'$')
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),'$')
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),'$')
else:
formula=formula.subs(var,end2+(end1-end2)/var)
print(sTranslation['Substitute'], "$",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):
if {interval[0],interval[1]} & {S('inf'),S('-inf')}==set():
num=num.subs(var,var+1)
den=den.subs(var,var+1)
equations=[equation.subs(var,var+1) for equation in equations]
if values:
values=ssolve(equations,variables)
if len(values):
values=values[0]
num,den=expand(num),expand(den)
#print(sTranslation["Formula after substitution:"],"$$",slatex(num/den),'$$')
if values and numden:
return num,den,values
elif values:
return num/den,values
elif numden:
return num,den
else:
return num/den
def _formula2listf(formula):
#Splits a polynomial to a difference of two formulas with positive
#coefficients and extracts coefficients and function
#arguments of both formulas.
lfun=[]
lcoef=[]
rfun=[]
rcoef=[]
for addend in formula.as_ordered_terms():
coef,facts=addend.as_coeff_mul()
if(coef<0):
lcoef+=[-coef]
lfun+=[facts[0].args]
else:
rcoef+=[coef]
rfun+=[facts[0].args]
return(lcoef,lfun,rcoef,rfun)
def provef(formula,niter=200,linprogiter=10000):
#this function is similar to prove, formula is a linear combination of
#values of f:R^k->R instead of a polynomial. provef checks if a formula
#is nonnegative for any nonnegative and convex function f. If so, it
#provides a proof of nonnegativity.
formula=S(formula)
num,den=_input2fraction(formula,[],[])
_list2proof(*(_formula2listf(num)+(None,niter,linprogiter,_writ)))
def issymetric(formula): #checks if formula is symmetric
#and has at least two variables
if len(formula.free_symbols)<2:
return False
ls=list(formula.free_symbols)
a=ls[0]
for b in ls[1:]:
if expand(formula-formula.subs({a:b, b:a}, simultaneous=True))!=S(0):
return False
return True
def cyclize(formula,oper=operator.add,variables=None,init=None):
#cyclize('a^2*b')=S('a^2*b+b^2*a')
#cyclize('a^2*b',variables='a,b,c')=S('a^2*b+b^2*c+c^2*a')
formula=S(formula)
if variables==None:
variables=sorted(formula.free_symbols,key=str)
else:
variables=S(variables)
if len(variables)==0:
return init
variables=list(variables) #if variables is a tuple, change it to a list
variables+=[variables[0]]
subst=list(zip(variables[:-1],variables[1:]))
if init==None:
init=formula
else:
init=oper(init,formula)
for _ in variables[2:]:
formula=formula.subs(subst,simultaneous=True)
init=oper(init,formula)
return init
def symmetrize(formula,oper=operator.add,variables=None,init=None):
#symmetrize('a^2*b')=S('a^2*b+b^2*a')
#symmetrize('a^2*b',variables='a,b,c')=
#=S('a^2*b+a^2*c+b^2*a+b^2*c+c^2*a+c^2*b')
formula=S(formula)
if variables==None:
variables=sorted(formula.free_symbols,key=str)
else:
variables=S(variables)
for i in range(1,len(variables)):
formula=cyclize(formula,oper,variables[:i+1])
return formula