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

added statistics and fixed few minor bugs

Browse Source
This commit is contained in:
urojony 2020-05-17 23:46:53 +02:00
parent 587bdd704c
commit f5e0cc14d4
11 changed files with 12183 additions and 2415 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2045
.ipynb_checkpoints/examples-checkpoint.ipynb
View File

File diff suppressed because it is too large Load Diff

2706
.ipynb_checkpoints/sandbox-checkpoint.ipynb
View File

File diff suppressed because it is too large Load Diff

476
.ipynb_checkpoints/statistics-checkpoint.ipynb Normal file
View File

@ -0,0 +1,476 @@
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"In this notebook several methods for proving inequalities have been compared.\n",
"\n",
"First of all we need a dataset. 35 inequalities were selected from https://www.imomath.com/index.php?options=592&lmm=0. Each inequality is represented by a tuple: inequality (in LaTeX), inequality constraints (for example: $a\\in [0,1]$, equality constraints (for example: $abc=1$) and a function which converts inequality to a formula which we want to prove it's nonnegativity. In most cases when this function is simply a difference between left and right-hand side, but sometimes it's better to use difference between squares of sides (to get rid of square roots). These tuples are used as parameters in `parser` function which converts them to equivalent inequalities with default constraints (i.e. all variables are positive).\n",
"\n",
"Some tuples have less than 4 elements. In this case `parser` use default arguments."
]
},
{
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [],
"source": [
"from importlib import reload\n",
"from sympy import *\n",
"import shiroindev\n",
"from shiroindev import *\n",
"from sympy.parsing.latex import parse_latex\n",
"shiro.seed=1\n",
"from IPython.display import Latex\n",
"shiro.display=lambda x:display(Latex(x))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"`sympy` has a `parse_latex` function which converts LaTeX formula to a `sympy` one. Unfortunately it doesn't deal with missing braces in the way that LaTeX do. For example `\\frac12` generates $\\frac12$ which is the same as `\\frac{1}{2}`, but `parse_latex` accepts only the second version. So here there is a boring function which adds missing braces."
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"\\frac{ \\sqrt {3}}{2}\n",
"a^2+b^2+c^2\\geq ab+bc+ca\n"
]
}
],
"source": [
"def addbraces(s):\n",
" arg={r'\\frac':2,r'\\sqrt':1}\n",
" s2=''\n",
" p=0\n",
" while 1:\n",
" m=re.search(r\"\\\\[a-zA-Z]+\", s[p:])\n",
" if not m:\n",
" break\n",
" s2+=s[p:p+m.end()]\n",
" #print('a',s[p:m.end()],p)\n",
" p+=m.end()\n",
" if m.group() in arg:\n",
" for i in range(arg[m.group()]):\n",
" sp=re.search('^ *',s[p:])\n",
" s2+=sp.group()\n",
" #print('b',sp.group(),p)\n",
" p+=sp.end()\n",
" if s[p]=='{':\n",
" cb=re.search(r'^\\{.*?\\}',s[p:])\n",
" ab=addbraces(cb.group())\n",
" s2+=ab\n",
" #print('c',ab,p)\n",
" p+=cb.end()\n",
" else:\n",
" s2+='{'+s[p]+'}'\n",
" #print('d','{'+s[p]+'}',p)\n",
" p+=1\n",
" #print('e',p)\n",
" s2+=s[p:]\n",
" return s2\n",
"print(addbraces(r'\\frac{ \\sqrt 3}2'))\n",
"print(addbraces(r'a^2+b^2+c^2\\geq ab+bc+ca'))"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [],
"source": [
"#(formula,intervals,subs,function)\n",
"dif=lambda b,s:b-s\n",
"dif2=lambda b,s:b*b-s*s\n",
"ineqs=[\n",
" (r'a^2+b^2+c^2\\geq ab+bc+ca',),\n",
" (r'a^2+b^2+c^2+d^2\\geq a(b+c+d)',),\n",
" (r'1\\leq\\frac{a^2b^2}{c^2}+\\frac{b^2c^2}{a^2}+\\frac{c^2a^2}{b^2}',\n",
" '[0,1-f],[0,1]','[a,sqrt(1-e-f)],[b,sqrt(e)],[c,sqrt(f)]',),\n",
" (r'\\frac1{1-x^2}+\\frac1{1-y^2}\\geq \\frac2{1-xy}','[0,1],[0,1]'),\n",
" (r'a^3+b^3\\geq a^2b+ab^2',),\n",
" (r'\\frac a{b+c}+\\frac b{c+a}+\\frac c{a+b}\\geq \\frac32',),\n",
" (r'2a^3+b^3\\geq 3a^2b',),\n",
" (r'a^3+b^3+c^3\\geq a^2b+b^2c+c^2a',),\n",
" (r'\\frac a{b+c}+\\frac b{c+d}+ \\frac c{d+a}+ \\frac d{a+b}\\geq 2',),\n",
" (r'\\frac{a^3}{a^2+ab+b^2}+ \\frac{b^3}{b^2+bc+c^2}+ \\frac{c^3}{c^2+ca+a^2} \\geq \\frac{a+b+c}3',),\n",
" (r'\\sqrt{ab}+\\sqrt{cd}+\\sqrt{ef}\\leq\\sqrt{(a+c+e)(b+d+f)}','','',dif2),\n",
" (r'\\frac{5a^3-ab^2}{a+b}+\\frac{5b^3-bc^2}{b+c}+\\frac{5c^3-ca^2}{c+a}\\geq 2(a^2+b^2+c^2)',),\n",
" #(r'\\frac{a^2}{(1+b)(1-c)}+\\frac{b^3}{(1+c)(1-d)}+\\frac{c^3}{(1+d)(1-a)}+\\frac{d^3}{(1+a)(1-b)}\\geq\\frac1{15}',\n",
" # '[0,1-c-d],[0,1-d],[0,1]','[a,1-b-c-d]'),\n",
" (r'\\frac{x^3}{(1+y)(1+z)}+\\frac{y^3}{(1+z)(1+x)}+\\frac{z^3}{(1+x)(1+y)}\\geq\\frac{3}{4}','','[z,1/(x*y)]'),\n",
" (r'\\frac ab+\\frac bc+\\frac ca\\geq \\frac{(a+b+c)^2}{ab+bc+ca}',),\n",
" (r'\\frac{a^2}b+\\frac{b^2}c+\\frac{c^2}a\\geq \\frac{a^2+b^2+c^2}{a+b+c}',),\n",
" (r'\\frac{a^2}b+\\frac{b^2}c+\\frac{c^2}a\\geq a+b+c+\\frac{4(a-b)^2}{a+b+c}',),\n",
" (r'\\frac1{a^3+b^3+abc}+ \\frac1{b^3+c^3+abc} +\\frac1{c^3+a^3+ abc} \\leq \\frac1{abc}',),\n",
" (r'\\frac1{a^3(b+c)}+ \\frac1{b^3(c+a)}+ \\frac1{c^3(a+b)} \\geq \\frac32','','[c,1/(a*b)]'),\n",
" (r'\\frac{a^3}{b^2-bc+c^2}+\\frac{b^3}{c^2-ca+a^2} + \\frac{c^3}{a^2-ab+b^2} \\geq 3 \\cdot\\frac{ab+bc+ca}{a+b+c}',),\n",
" (r'\\frac{x^5-x^2}{x^5+y^2+z^2}+\\frac{y^5-y^2}{y^5+z^2+x^2}+\\frac{z^5-z^2}{z^5+x^2+y^2}\\geq0','','[x,1/(y*z)]'),\n",
" (r'(a+b-c)(b+c-a)(c+a-b)\\leq abc',),\n",
" (r'\\frac1{1+xy}+\\frac1{1+yz}+\\frac1{1+zx}\\leq \\frac34','','[x,(y+z)/(y*z-1)]'),\n",
" (r'\\frac{x\\sqrt x}{y+z}+\\frac{y\\sqrt y}{z+x}+\\frac{z\\sqrt z}{x+y}\\geq\\frac{ \\sqrt 3}2',\n",
" '[0,1-z],[0,1]','[x,1-y-z]'),\n",
" (r'a^4+b^4+c^4+d^4\\geq 4abcd',),\n",
" (r'\\frac{ab}{a+b}+\\frac{bc}{b+c}+\\frac{ca}{c+a}\\leq\\frac{3(ab+bc+ca)}{2(a+b+c)}',),\n",
" (r'\\sqrt{a-1}+\\sqrt{b-1}+ \\sqrt{c-1} \\leq \\sqrt{c(ab+1)}','[1,oo],[1,oo],[1,oo]','',dif2),\n",
" (r'(x-1)(y-1)(z-1)\\geq 8','[0,1-b-c],[0,1-c],[0,1]','[x,1/a],[y,1/b],[z,1/c]'),\n",
" (r'ay+bz+cx\\leq s^2','[0,s],[0,s],[0,s]','[x,s-a],[y,s-b],[z,s-c]'),\n",
" (r'x_1^2+x_2^2+x_3^2+x_4^2+x_5^2\\geq 2 (x_1x_2+x_2x_3+x_3x_4+x_4x_5)/\\sqrt{3}',),\n",
" (r' xy+yz+zx - 2xyz \\leq \\frac7{27}', '[0,1-z],[0,1]','[x,1-y-z]'),\n",
" (r'0 \\leq xy+yz+zx - 2xyz', '[0,1-z],[0,1]','[x,1-y-z]'),\n",
" (r'\\sqrt{3+a+b+c}\\geq\\sqrt a+\\sqrt b+\\sqrt c','[1-z,1],[0,1]','[a,1/x-1],[b,1/y-1],[c,1/z-1],[x,2-y-z]',\n",
" dif2),\n",
" (r'\\frac{2a^3}{a^2+b^2}+\\frac{2b^3}{b^2+c^2}+\\frac{2c^3}{c^2+a^2}\\geq a+b+c',),\n",
" (r'\\frac{a^2}{b+c}+\\frac{b^2}{c+a}+\\frac{c^2}{a+b}\\geq \\frac12','[0,1-c],[0,1]','[a,1-b-c]'),\n",
" (r'\\frac{a+b}{2b+c}+\\frac{b+c}{2c+a}+\\frac{c+a}{2a+b}\\geq 2',),\n",
" #(r'\\frac x{5-y^2}+\\frac y{5-z^2}+\\frac z{5-x^2}\\geq \\frac34','[0,sqrt(5)],[0,sqrt(5)]','[x,1/(y*z)]')\n",
"]\n",
"\n"
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [],
"source": [
"def parser(formula,intervals='[]',subs='[]',func=dif):\n",
" newproof()\n",
" shiro.display=lambda x:None\n",
" #display=lambda x:None\n",
" if intervals=='':\n",
" intervals='[]'\n",
" if subs=='':\n",
" subs='[]'\n",
" formula=addbraces(formula)\n",
" formula=Sm(str(parse_latex(formula)))\n",
" formula,_=fractioncancel(formula)\n",
" formula=formula.subs(shiroindev._smakeiterable2(subs))\n",
" formula=makesubs(formula,intervals)\n",
" b,s=formula.lhs,formula.rhs\n",
" if type(formula)==LessThan:\n",
" b,s=s,b\n",
" formula=func(b,s)\n",
" formula=simplify(formula)\n",
" num,den=fractioncancel(formula)\n",
" return num"
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"name": "stderr",
"output_type": "stream",
"text": [
" 74%|███████▍ | 26/35 [00:21<00:07, 1.21it/s]\n"
]
},
{
"ename": "KeyboardInterrupt",
"evalue": "",
"output_type": "error",
"traceback": [
"\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
"\u001b[0;31mKeyboardInterrupt\u001b[0m Traceback (most recent call last)",
"\u001b[0;32m<ipython-input-5-099273dd73e0>\u001b[0m in \u001b[0;36m<module>\u001b[0;34m()\u001b[0m\n\u001b[1;32m 2\u001b[0m \u001b[0mineqs2\u001b[0m\u001b[0;34m=\u001b[0m\u001b[0;34m[\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 3\u001b[0m \u001b[0;32mfor\u001b[0m \u001b[0mineq\u001b[0m \u001b[0;32min\u001b[0m \u001b[0mtqdm\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mineqs\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m----> 4\u001b[0;31m \u001b[0mineqs2\u001b[0m\u001b[0;34m+=\u001b[0m\u001b[0;34m[\u001b[0m\u001b[0mparser\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m*\u001b[0m\u001b[0mineq\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m",
"\u001b[0;32m<ipython-input-4-03e6aa4471bf>\u001b[0m in \u001b[0;36mparser\u001b[0;34m(formula, intervals, subs, func)\u001b[0m\n\u001b[1;32m 16\u001b[0m \u001b[0mb\u001b[0m\u001b[0;34m,\u001b[0m\u001b[0ms\u001b[0m\u001b[0;34m=\u001b[0m\u001b[0ms\u001b[0m\u001b[0;34m,\u001b[0m\u001b[0mb\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 17\u001b[0m \u001b[0mformula\u001b[0m\u001b[0;34m=\u001b[0m\u001b[0mfunc\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mb\u001b[0m\u001b[0;34m,\u001b[0m\u001b[0ms\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m---> 18\u001b[0;31m \u001b[0mformula\u001b[0m\u001b[0;34m=\u001b[0m\u001b[0msimplify\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mformula\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 19\u001b[0m \u001b[0mnum\u001b[0m\u001b[0;34m,\u001b[0m\u001b[0mden\u001b[0m\u001b[0;34m=\u001b[0m\u001b[0mfractioncancel\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mformula\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 20\u001b[0m \u001b[0;32mreturn\u001b[0m \u001b[0mnum\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
"\u001b[0;32m/home/grzegorz/Pobrane/SageMath/local/lib/python3.7/site-packages/sympy/simplify/simplify.py\u001b[0m in \u001b[0;36msimplify\u001b[0;34m(expr, ratio, measure, rational, inverse)\u001b[0m\n\u001b[1;32m 560\u001b[0m \u001b[0m_e\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mcancel\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mexpr\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 561\u001b[0m \u001b[0mexpr1\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mshorter\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0m_e\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0m_mexpand\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0m_e\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mcancel\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;31m# issue 6829\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 562\u001b[0;31m \u001b[0mexpr2\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mshorter\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mtogether\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mexpr\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mdeep\u001b[0m\u001b[0;34m=\u001b[0m\u001b[0;32mTrue\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mtogether\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mexpr1\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mdeep\u001b[0m\u001b[0;34m=\u001b[0m\u001b[0;32mTrue\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 563\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 564\u001b[0m \u001b[0;32mif\u001b[0m \u001b[0mratio\u001b[0m \u001b[0;32mis\u001b[0m \u001b[0mS\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mInfinity\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
"\u001b[0;32m/home/grzegorz/Pobrane/SageMath/local/lib/python3.7/site-packages/sympy/polys/rationaltools.py\u001b[0m in \u001b[0;36mtogether\u001b[0;34m(expr, deep, fraction)\u001b[0m\n\u001b[1;32m 83\u001b[0m \u001b[0;32mreturn\u001b[0m \u001b[0mexpr\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 84\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m---> 85\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0m_together\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0msympify\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mexpr\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m",
"\u001b[0;32m/home/grzegorz/Pobrane/SageMath/local/lib/python3.7/site-packages/sympy/polys/rationaltools.py\u001b[0m in \u001b[0;36m_together\u001b[0;34m(expr)\u001b[0m\n\u001b[1;32m 77\u001b[0m \u001b[0;32mreturn\u001b[0m \u001b[0mexpr\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0m__class__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mbase\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mexp\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 78\u001b[0m \u001b[0;32melse\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m---> 79\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0mexpr\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0m__class__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m*\u001b[0m\u001b[0;34m[\u001b[0m \u001b[0m_together\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0marg\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;32mfor\u001b[0m \u001b[0marg\u001b[0m \u001b[0;32min\u001b[0m \u001b[0mexpr\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0margs\u001b[0m \u001b[0;34m]\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 80\u001b[0m \u001b[0;32melif\u001b[0m \u001b[0miterable\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mexpr\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 81\u001b[0m \u001b[0;32mreturn\u001b[0m \u001b[0mexpr\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0m__class__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m[\u001b[0m \u001b[0m_together\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mex\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;32mfor\u001b[0m \u001b[0mex\u001b[0m \u001b[0;32min\u001b[0m \u001b[0mexpr\u001b[0m \u001b[0;34m]\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
"\u001b[0;32m/home/grzegorz/Pobrane/SageMath/local/lib/python3.7/site-packages/sympy/polys/rationaltools.py\u001b[0m in \u001b[0;36m<listcomp>\u001b[0;34m(.0)\u001b[0m\n\u001b[1;32m 77\u001b[0m \u001b[0;32mreturn\u001b[0m \u001b[0mexpr\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0m__class__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mbase\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mexp\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 78\u001b[0m \u001b[0;32melse\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m---> 79\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0mexpr\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0m__class__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m*\u001b[0m\u001b[0;34m[\u001b[0m \u001b[0m_together\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0marg\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;32mfor\u001b[0m \u001b[0marg\u001b[0m \u001b[0;32min\u001b[0m \u001b[0mexpr\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0margs\u001b[0m \u001b[0;34m]\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 80\u001b[0m \u001b[0;32melif\u001b[0m \u001b[0miterable\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mexpr\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 81\u001b[0m \u001b[0;32mreturn\u001b[0m \u001b[0mexpr\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0m__class__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m[\u001b[0m \u001b[0m_together\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mex\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;32mfor\u001b[0m \u001b[0mex\u001b[0m \u001b[0;32min\u001b[0m \u001b[0mexpr\u001b[0m \u001b[0;34m]\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
"\u001b[0;32m/home/grzegorz/Pobrane/SageMath/local/lib/python3.7/site-packages/sympy/polys/rationaltools.py\u001b[0m in \u001b[0;36m_together\u001b[0;34m(expr)\u001b[0m\n\u001b[1;32m 66\u001b[0m \u001b[0;32mreturn\u001b[0m \u001b[0mexpr\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 67\u001b[0m \u001b[0;32melif\u001b[0m \u001b[0mexpr\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mis_Add\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m---> 68\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0mgcd_terms\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mlist\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mmap\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0m_together\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mAdd\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mmake_args\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mexpr\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mfraction\u001b[0m\u001b[0;34m=\u001b[0m\u001b[0mfraction\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 69\u001b[0m \u001b[0;32melif\u001b[0m \u001b[0mexpr\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mis_Pow\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 70\u001b[0m \u001b[0mbase\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0m_together\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mexpr\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mbase\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
"\u001b[0;32m/home/grzegorz/Pobrane/SageMath/local/lib/python3.7/site-packages/sympy/polys/rationaltools.py\u001b[0m in \u001b[0;36m_together\u001b[0;34m(expr)\u001b[0m\n\u001b[1;32m 77\u001b[0m \u001b[0;32mreturn\u001b[0m \u001b[0mexpr\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0m__class__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mbase\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mexp\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 78\u001b[0m \u001b[0;32melse\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m---> 79\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0mexpr\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0m__class__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m*\u001b[0m\u001b[0;34m[\u001b[0m \u001b[0m_together\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0marg\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;32mfor\u001b[0m \u001b[0marg\u001b[0m \u001b[0;32min\u001b[0m \u001b[0mexpr\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0margs\u001b[0m \u001b[0;34m]\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 80\u001b[0m \u001b[0;32melif\u001b[0m \u001b[0miterable\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mexpr\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 81\u001b[0m \u001b[0;32mreturn\u001b[0m \u001b[0mexpr\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0m__class__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m[\u001b[0m \u001b[0m_together\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mex\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;32mfor\u001b[0m \u001b[0mex\u001b[0m \u001b[0;32min\u001b[0m \u001b[0mexpr\u001b[0m \u001b[0;34m]\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
"\u001b[0;32m/home/grzegorz/Pobrane/SageMath/local/lib/python3.7/site-packages/sympy/polys/rationaltools.py\u001b[0m in \u001b[0;36m<listcomp>\u001b[0;34m(.0)\u001b[0m\n\u001b[1;32m 77\u001b[0m \u001b[0;32mreturn\u001b[0m \u001b[0mexpr\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0m__class__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mbase\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mexp\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 78\u001b[0m \u001b[0;32melse\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m---> 79\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0mexpr\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0m__class__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m*\u001b[0m\u001b[0;34m[\u001b[0m \u001b[0m_together\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0marg\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;32mfor\u001b[0m \u001b[0marg\u001b[0m \u001b[0;32min\u001b[0m \u001b[0mexpr\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0margs\u001b[0m \u001b[0;34m]\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 80\u001b[0m \u001b[0;32melif\u001b[0m \u001b[0miterable\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mexpr\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 81\u001b[0m \u001b[0;32mreturn\u001b[0m \u001b[0mexpr\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0m__class__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m[\u001b[0m \u001b[0m_together\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mex\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;32mfor\u001b[0m \u001b[0mex\u001b[0m \u001b[0;32min\u001b[0m \u001b[0mexpr\u001b[0m \u001b[0;34m]\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
"\u001b[0;32m/home/grzegorz/Pobrane/SageMath/local/lib/python3.7/site-packages/sympy/polys/rationaltools.py\u001b[0m in \u001b[0;36m_together\u001b[0;34m(expr)\u001b[0m\n\u001b[1;32m 66\u001b[0m \u001b[0;32mreturn\u001b[0m \u001b[0mexpr\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 67\u001b[0m \u001b[0;32melif\u001b[0m \u001b[0mexpr\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mis_Add\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m---> 68\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0mgcd_terms\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mlist\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mmap\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0m_together\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mAdd\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mmake_args\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mexpr\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mfraction\u001b[0m\u001b[0;34m=\u001b[0m\u001b[0mfraction\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 69\u001b[0m \u001b[0;32melif\u001b[0m \u001b[0mexpr\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mis_Pow\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 70\u001b[0m \u001b[0mbase\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0m_together\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mexpr\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mbase\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
"\u001b[0;32m/home/grzegorz/Pobrane/SageMath/local/lib/python3.7/site-packages/sympy/core/exprtools.py\u001b[0m in \u001b[0;36mgcd_terms\u001b[0;34m(terms, isprimitive, clear, fraction)\u001b[0m\n\u001b[1;32m 1061\u001b[0m \u001b[0mterms\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0msympify\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mterms\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 1062\u001b[0m \u001b[0mterms\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mreps\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mmask\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mterms\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m-> 1063\u001b[0;31m \u001b[0mcont\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mnumer\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mdenom\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0m_gcd_terms\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mterms\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0misprimitive\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mfraction\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 1064\u001b[0m \u001b[0mnumer\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mnumer\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mxreplace\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mreps\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 1065\u001b[0m \u001b[0mcoeff\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mfactors\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mcont\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mas_coeff_Mul\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
"\u001b[0;32m/home/grzegorz/Pobrane/SageMath/local/lib/python3.7/site-packages/sympy/core/exprtools.py\u001b[0m in \u001b[0;36m_gcd_terms\u001b[0;34m(terms, isprimitive, fraction)\u001b[0m\n\u001b[1;32m 954\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 955\u001b[0m \u001b[0;32mfor\u001b[0m \u001b[0mi\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mterm\u001b[0m \u001b[0;32min\u001b[0m \u001b[0menumerate\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mterms\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 956\u001b[0;31m \u001b[0mterms\u001b[0m\u001b[0;34m[\u001b[0m\u001b[0mi\u001b[0m\u001b[0;34m]\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mterm\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mquo\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mcont\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 957\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 958\u001b[0m \u001b[0;32mif\u001b[0m \u001b[0mfraction\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
"\u001b[0;32m/home/grzegorz/Pobrane/SageMath/local/lib/python3.7/site-packages/sympy/core/exprtools.py\u001b[0m in \u001b[0;36mquo\u001b[0;34m(self, other)\u001b[0m\n\u001b[1;32m 872\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 873\u001b[0m \u001b[0;32mdef\u001b[0m \u001b[0mquo\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mother\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m:\u001b[0m \u001b[0;31m# Term\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 874\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0mself\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mmul\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mother\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0minv\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 875\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 876\u001b[0m \u001b[0;32mdef\u001b[0m \u001b[0mpow\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mother\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m:\u001b[0m \u001b[0;31m# Term\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
"\u001b[0;32m/home/grzegorz/Pobrane/SageMath/local/lib/python3.7/site-packages/sympy/core/exprtools.py\u001b[0m in \u001b[0;36mmul\u001b[0;34m(self, other)\u001b[0m\n\u001b[1;32m 864\u001b[0m \u001b[0mdenom\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mself\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mdenom\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mmul\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mother\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mdenom\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 865\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 866\u001b[0;31m \u001b[0mnumer\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mdenom\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mnumer\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mnormal\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mdenom\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 867\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 868\u001b[0m \u001b[0;32mreturn\u001b[0m \u001b[0mTerm\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mcoeff\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mnumer\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mdenom\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
"\u001b[0;32m/home/grzegorz/Pobrane/SageMath/local/lib/python3.7/site-packages/sympy/core/exprtools.py\u001b[0m in \u001b[0;36mnormal\u001b[0;34m(self, other)\u001b[0m\n\u001b[1;32m 556\u001b[0m \u001b[0;32mdel\u001b[0m \u001b[0mother_factors\u001b[0m\u001b[0;34m[\u001b[0m\u001b[0mfactor\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 557\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 558\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0mFactors\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself_factors\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mFactors\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mother_factors\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 559\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 560\u001b[0m \u001b[0;32mdef\u001b[0m \u001b[0mdiv\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mother\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m:\u001b[0m \u001b[0;31m# Factors\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
"\u001b[0;32m/home/grzegorz/Pobrane/SageMath/local/lib/python3.7/site-packages/sympy/core/exprtools.py\u001b[0m in \u001b[0;36m__init__\u001b[0;34m(self, factors)\u001b[0m\n\u001b[1;32m 367\u001b[0m \u001b[0mhandle\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0;34m[\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 368\u001b[0m \u001b[0;32mfor\u001b[0m \u001b[0mk\u001b[0m \u001b[0;32min\u001b[0m \u001b[0mfactors\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 369\u001b[0;31m \u001b[0;32mif\u001b[0m \u001b[0mk\u001b[0m \u001b[0;32mis\u001b[0m \u001b[0mI\u001b[0m \u001b[0;32mor\u001b[0m \u001b[0mk\u001b[0m \u001b[0;32min\u001b[0m \u001b[0;34m(\u001b[0m\u001b[0;34m-\u001b[0m\u001b[0;36m1\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;36m1\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 370\u001b[0m \u001b[0mhandle\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mappend\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mk\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 371\u001b[0m \u001b[0;32mif\u001b[0m \u001b[0mhandle\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
"\u001b[0;32m/home/grzegorz/Pobrane/SageMath/local/lib/python3.7/site-packages/sympy/core/basic.py\u001b[0m in \u001b[0;36m__eq__\u001b[0;34m(self, other)\u001b[0m\n\u001b[1;32m 333\u001b[0m \u001b[0;31m# (https://github.com/sympy/sympy/issues/4269), we only compare\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 334\u001b[0m \u001b[0;31m# types in Python 2 directly if they actually have __ne__.\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 335\u001b[0;31m \u001b[0;32mif\u001b[0m \u001b[0mPY3\u001b[0m \u001b[0;32mor\u001b[0m \u001b[0mtype\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mtself\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0m__ne__\u001b[0m \u001b[0;32mis\u001b[0m \u001b[0;32mnot\u001b[0m \u001b[0mtype\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0m__ne__\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 336\u001b[0m \u001b[0;32mif\u001b[0m \u001b[0mtself\u001b[0m \u001b[0;34m!=\u001b[0m \u001b[0mtother\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 337\u001b[0m \u001b[0;32mreturn\u001b[0m \u001b[0;32mFalse\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
"\u001b[0;31mKeyboardInterrupt\u001b[0m: "
]
}
],
"source": [
"from tqdm import tqdm\n",
"ineqs2=[]\n",
"for ineq in tqdm(ineqs):\n",
" ineqs2+=[parser(*ineq)]"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Now let's look at the formulas when converted to polynomials."
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"for i,ineq in zip(range(len(ineqs2)),ineqs2):\n",
" print(i)\n",
" display(reducegens(assumeall(ineq,positive=True)))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Most formulas was converted to polynomials of independent variables. However formulas No. 22 and No. 31 were not. For this reason it's very unlikely that any method of proving these ones will succeed.\n",
"\n",
"Now let's try some methods of proving these inequalities. The first one would be the simple `prove`."
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"tm=[0]*4"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"from collections import Counter\n",
"from timeit import default_timer as timer\n",
"start=timer()\n",
"t=[]\n",
"for ineq in ineqs2:\n",
" t+=[prove(ineq)]\n",
" print(t[-1],end=',')\n",
"tm[0]=timer()-start\n",
"print('\\n',tm[0],sep='')\n",
"Counter(t)\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Code 0 means that the proof was found, all other codes means that proof wasn't found. So this method has proved 21 inequalities.\n",
"\n",
"The second method uses `findvalues` function, rationalizes the result numbers and gives them as additional parameter to `prove` function."
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"def cut(a):\n",
" if a<=0 or a>=100 or (a is None):\n",
" return 1\n",
" return a\n",
"start=timer()\n",
"t2=[]\n",
"for ineq in ineqs2:\n",
" numvalues=findvalues(ineq,disp=0)\n",
" values=nsimplify(numvalues,tolerance=0.1,rational=True)\n",
" values=list(map(cut,values))\n",
" t2+=[prove(ineq,values=values)]\n",
" print(t2[-1],end=',')\n",
"tm[1]=timer()-start\n",
"print('\\n',tm[1],sep='')\n",
"Counter(t2)\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The third method is similar to the second one, but instead of rationalize values it squares, rationalizes and makes square roots of these values."
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"def cut(a):\n",
" if a<=0 or a>=1000 or (a is None):\n",
" return S(1)\n",
" return a\n",
" \n",
"start=timer()\n",
"t3=[]\n",
"for ineq in ineqs2:\n",
" numvalues=findvalues(ineq,disp=0)\n",
" numvalues=tuple([x**2 for x in numvalues])\n",
" values=nsimplify(numvalues,tolerance=0.1,rational=True)\n",
" values=[sqrt(x) for x in values]\n",
" values=list(map(cut,values))\n",
" t3+=[prove(ineq,values=values)]\n",
" print(t3[-1],end=',')\n",
"tm[2]=timer()-start\n",
"print('\\n',tm[2],sep='')\n",
"Counter(t3)\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Finally, the fourth method is a slight modification to the third method. It does the same \"findvalues, square, rationalize and make square roots\" thing, but then it scales the values and runs it again. It can sometimes help with uniform formulas."
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"def betw(a):\n",
" return a>0.001 and a<1000 and a!=None\n",
"def cut(a):\n",
" if betw(a):\n",
" return a\n",
" return S(1)\n",
"\n",
"start=timer()\n",
"t4=[]\n",
"for ineq in ineqs2:\n",
" numvalues=findvalues(ineq,disp=0)\n",
" n=1\n",
" numvalues2=[]\n",
" for i in numvalues:\n",
" if betw(i):\n",
" n=1/i\n",
" break\n",
" for i in numvalues:\n",
" if betw(i):\n",
" numvalues2+=[i*n]\n",
" else:\n",
" numvalues2+=[1]\n",
" numvalues3=findvalues(ineq,values=numvalues2,disp=0)\n",
" numvalues4=tuple([x**2 for x in numvalues3])\n",
" values=nsimplify(numvalues4,tolerance=0.1,rational=True)\n",
" values=[sqrt(x) for x in values]\n",
" values=list(map(cut,values))\n",
" t4+=[prove(ineq,values=values)]\n",
" print(t4[-1],end=',')\n",
"tm[3]=timer()-start\n",
"print('\\n',tm[3],sep='')\n",
"Counter(t4)"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"import matplotlib.pyplot as plt\n",
"plt.bar(['1','2','3','4'],tm)\n",
"plt.ylabel('time [seconds]')\n",
"plt.xlabel('method')\n",
"plt.show()"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"import pandas as pd\n",
"u=pd.DataFrame(zip(['']*len(ineqs),t,t2,t3,t4))"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"plt.bar(['1','2','3','4'],[sum(u[i]==0)/len(ineqs2)*100 for i in range(1,5)])\n",
"plt.ylabel('inequalities proven [%]')\n",
"plt.xlabel('method')\n",
"plt.show()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Down below there are contingency tables and McNemar test for every pair of methods."
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"for i in range(4):\n",
" for j in range(i+1,4):\n",
" display(pd.crosstab(u[i+1]==0, u[j+1]==0))"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"from statsmodels.stats.contingency_tables import mcnemar\n",
"for i in range(4):\n",
" for j in range(i+1,4):\n",
" print(mcnemar(pd.crosstab(u[i+1]==0, u[j+1]==0)))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"In all cases p-value is greater than 0.05, so there is no statistical difference between the methods."
]
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3",
"language": "python",
"name": "python3"
},
"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-36.pyc
View File

Binary file not shown.

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

Binary file not shown.

380
examples.ipynb
View File

File diff suppressed because it is too large Load Diff

BIN
examples.pdf
View File

Binary file not shown.

7076
sandbox.ipynb
View File

File diff suppressed because it is too large Load Diff

352
shiroindev.py
View File

@ -2,14 +2,28 @@ from __future__ import (absolute_import, division,
print_function, unicode_literals) print_function, unicode_literals)
import warnings,operator import warnings,operator
warnings.filterwarnings("ignore") warnings.filterwarnings("ignore")
#Seed is needed to select the weights in linprog function. def vargen(n):
#None means that the seed is random. """default function generating names for variables"""
q=len(shiro.alphabet)
x=shiro.alphabet[n%q]
if n>=q:
x+=str(n//q)
return x
class Vars: class Vars:
pass pass
sVars=Vars() shiro=Vars()
sVars.display=print shiro.display=shiro.warning=print
sVars.seed=None shiro.seed=None
sVars.translation={} """Seed is needed to select the weights in linprog function.
None means that the seed is random"""
shiro.translation={}
shiro.varind=0
shiro.varset=set()
"""set of used symbols in the proof"""
shiro.vargen=vargen
"""function generating names for variables"""
shiro.alphabet='abcdefghijklmnopqrstuvwxyz'
"""list of names for variables"""
translationList=['numerator:','denominator:','status:', translationList=['numerator:','denominator:','status:',
'Substitute',"Formula after substitution:", 'Substitute',"Formula after substitution:",
"Numerator after substitutions:","From weighted AM-GM inequality:", "Numerator after substitutions:","From weighted AM-GM inequality:",
@ -19,22 +33,38 @@ translationList=['numerator:','denominator:','status:',
"Program couldn't find any proof.", "Program couldn't find any proof.",
"Try to set higher linprogiter parameter.", "Try to set higher linprogiter parameter.",
"It looks like the formula is symmetric. You can assume without loss of"+ "It looks like the formula is symmetric. You can assume without loss of"+
" generality that ","Try", 'From Jensen inequality:' " generality that ","Try", 'From Jensen inequality:',
'Warning: intervals contain backwards dependencies. Consider changing order of variables and intervals.'
] ]
#Initialize english-english dictionary. #Initialize english-english dictionary.
for phrase in translationList: for phrase in translationList:
sVars.translation[phrase]=phrase shiro.translation[phrase]=phrase
from scipy.optimize import linprog,fmin from scipy.optimize import linprog,fmin
import random import random
from sympy import S,cancel,fraction,Pow,expand,solve,latex,oo,Poly,lambdify from sympy import S,cancel,fraction,Pow,expand,solve,latex,oo,Poly,lambdify,srepr,gcd,Symbol
from sympy.parsing.sympy_parser import parse_expr, standard_transformations,\
implicit_multiplication_application, convert_xor
from collections import Counter from collections import Counter
import re import re
def addsymbols(formula):
formula=S(formula)
funcsymbols=[x[10:-2] for x in re.findall(r"Function\(\'.*?\'\)",srepr(formula))]
shiro.varset|=set(funcsymbols)|set(map(str,formula.free_symbols))
def newvar():
while 1:
x=shiro.vargen(shiro.varind)
shiro.varind+=1
if x not in shiro.varset:
return S(x)
def newproof():
shiro.varset=set()
shiro.varind=0
def _remzero(coef,fun): def _remzero(coef,fun):
#coef, fun represents an expression. """coef, fun represents an expression.
#For example, if expression=5f(2,3)+0f(4,6)+8f(1,4) 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]] then coef=[5,0,8], fun=[[2,3],[4,6],[1,4]]
#_remzero removes addends with coefficient equal to zero. _remzero removes addends with coefficient equal to zero.
#In this example ncoef=[5,8], nfun=[[2,3],[1,4]] In this example ncoef=[5,8], nfun=[[2,3],[1,4]]"""
ncoef=[] ncoef=[]
nfun=[] nfun=[]
for c,f in zip(coef,fun): for c,f in zip(coef,fun):
@ -42,11 +72,11 @@ def _remzero(coef,fun):
ncoef+=[c] ncoef+=[c]
nfun+=[f] nfun+=[f]
return ncoef,nfun return ncoef,nfun
def slatex(formula): #fancy function which makes latex code more readable, but still correct # ~ def slatex(formula): #fancy function which makes latex code more readable, but still correct
formula=re.sub(r'\^{(.)}',r'^\1',latex(formula,fold_short_frac=True).replace(' ','').replace('\\left(','(').replace('\\right)',')')) # ~ formula=re.sub(r'\^{(.)}',r'^\1',latex(formula,fold_short_frac=True).replace(' ','').replace('\\left(','(').replace('\\right)',')'))
return re.sub(r'\{(\(.+?\))\}',r'\1',formula) # ~ return re.sub(r'\{(\(.+?\))\}',r'\1',formula)
def _writ2(coef,fun,variables): def _writ2(coef,fun,variables):
return slatex(S((str(coef)+'*'+'*'.join([str(x)+'^'+str(y) for x,y in zip(variables,fun)])))) return latex(Poly({fun:coef},gens=variables).as_expr())
def _writ(coef,fun,nullvar): def _writ(coef,fun,nullvar):
return str(coef)+'f('+str(fun)[1:-1-(len(fun)==1)]+')' return str(coef)+'f('+str(fun)[1:-1-(len(fun)==1)]+')'
def _check(coef,fun,res,rfun): def _check(coef,fun,res,rfun):
@ -61,19 +91,35 @@ def _powr(formula):
else: else:
return [formula,S('1')] return [formula,S('1')]
def fractioncancel(formula): def fractioncancel(formula):
#workaround for buggy cancel function """workaround for buggy cancel function"""
num,den=fraction(cancel(formula/S('tmp'))) num,den=fraction(cancel(formula/S('tmp')))
den=den.subs(S('tmp'),S('1')) den=den.subs(S('tmp'),S('1'))
return num,den return num,den
def ssolve(formula,variables): def ssolve(formula,variables):
#workaround for inconsistent solve function """workaround for inconsistent solve function"""
result=solve(formula,variables) result=solve(formula,variables)
if type(result)==dict: if type(result)==dict:
result=[[result[var] for var in variables]] result=[[result[var] for var in variables]]
return result return result
def sstr(formula): #def sstr(formula):
return str(formula).replace('**','^').replace('*','').replace(' ','') # return str(formula).replace('**','^').replace('*','').replace(' ','')
def assumeall(formula,**kwargs):
"""Adds assumptions to all free symbols in formula.
>>> assumeall('sqrt(x*y)-sqrt(x)*sqrt(y)',positive=True)
0
"""
formula=S(formula)
fs=formula.free_symbols
for x in fs:
y=Symbol(str(x),**kwargs)
formula=formula.subs(x,y)
return formula
def reducegens(formula): def reducegens(formula):
"""Reduces size of the generator of the polynomial
>>>Poly('x+sqrt(x)')
Poly(x + (sqrt(x)), x, sqrt(x), domain='ZZ')
>>>reducegens('x+sqrt(x)')
Poly((sqrt(x))**2 + (sqrt(x)), sqrt(x), domain='ZZ') """
pol=Poly(formula) pol=Poly(formula)
newgens={} newgens={}
ind={} ind={}
@ -96,82 +142,90 @@ def reducegens(formula):
newpol=newpol.replace(ind[gen],gen**newgens[gen]) newpol=newpol.replace(ind[gen],gen**newgens[gen])
return newpol return newpol
def Sm(formula): def Sm(formula):
#Adds multiplication signs and sympifies a formula. """Adds multiplication signs and sympifies a formula.
#For example, Sm('(2x+y)(7+5xz)') -> S('(2*x+y)*(7+5*x*z)') For example, Sm('(2x+y)(7+5xz)') -> S('(2*x+y)*(7+5*x*z)')"""
if type(formula)==str: if type(formula)!=str:
formula=formula.replace(' ','') if _isiterable(formula): return type(formula)(map(Sm,formula))
for i in range(2): else: return S(formula)
formula=re.sub(r'([0-9a-zA-Z)])([(a-zA-Z])',r'\1*\2',formula) formula=formula.translate({ord('{'):None,ord('}'):' '})
formula=S(formula) transformations = (standard_transformations +(implicit_multiplication_application,convert_xor))
return formula return parse_expr(formula, transformations=transformations)
# ~ 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=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): def _input2fraction(formula,variables,values):
#makes some substitutions and converts formula to a fraction """makes some substitutions and converts formula to a fraction
#with expanded numerator and denominator with expanded numerator and denominator"""
formula=S(formula) formula=S(formula)
subst=[] subst=[]
for x,y in zip(variables,values): for x,y in zip(variables,values):
if y!=1: if y!=1:
sVars.display(sVars.translation['Substitute']+' $'+str(x)+'\\to '+slatex(S(y)*S(x))+'$') z=newvar()
subst+=[(x,x*y)] shiro.display(shiro.translation['Substitute']+' $'+latex(x)+'\\to '+latex(S(y)*S(z))+'$')
subst+=[(x,z*y)]
formula=formula.subs(subst) formula=formula.subs(subst)
numerator,denominator=fractioncancel(formula) numerator,denominator=fractioncancel(formula)
sVars.display(sVars.translation['numerator:']+' $'+slatex(numerator)+'$') shiro.display(shiro.translation['numerator:']+' $'+latex(numerator)+'$')
sVars.display(sVars.translation['denominator:']+' $'+slatex(denominator)+'$') shiro.display(shiro.translation['denominator:']+' $'+latex(denominator)+'$')
return (numerator,denominator) return (numerator,denominator)
def _formula2list(formula): def _formula2list(formula):
#Splits a polynomial to a difference of two polynomials with positive """Splits a polynomial to a difference of two polynomials with positive
#coefficients and extracts coefficients and powers of both polynomials. coefficients and extracts coefficients and powers of both polynomials.
#'variables' is used to set order of powers 'variables' is used to set order of powers
#For example, If formula=5x^2-4xy+8y^3, variables=[x,y], then For example, If formula=5x^2-4xy+8y^3, variables=[x,y], then
#the program tries to prove that the program tries to prove that
#0<=5x^2-4xy+8y^3 0<=5x^2-4xy+8y^3
#4xy<=5x^2+8y^3 4xy<=5x^2+8y^3
#returns [4],[(1,1)], [5,8],[(2,0),(0,3)], (x,y) returns [4],[(1,1)], [5,8],[(2,0),(0,3)], (x,y)"""
formula=reducegens(formula) formula=reducegens(assumeall(formula,positive=True))
neg=(formula.abs()-formula)/2 neg=(formula.abs()-formula)*S('1/2')
pos=(formula.abs()+formula)/2 pos=(formula.abs()+formula)*S('1/2')
neg=Poly(neg,gens=formula.gens)
pos=Poly(pos,gens=formula.gens)
return neg.coeffs(),neg.monoms(),pos.coeffs(),pos.monoms(),Poly(formula).gens return neg.coeffs(),neg.monoms(),pos.coeffs(),pos.monoms(),Poly(formula).gens
def _list2proof(lcoef,lfun,rcoef,rfun,variables,itermax,linprogiter,_writ2=_writ2,theorem="From weighted AM-GM inequality:"): 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. """Now the formula is splitted on two polynomials with positive coefficients.
#we will call them LHS and RHS and our inequality to prove would we will call them LHS and RHS and our inequality to prove would
#be LHS<=RHS (instead of 0<=RHS-LHS). 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)
#suppose we are trying to prove that The sketch of the algorithm.
#30x^2y^2+60xy^4<=48x^3+56y^6 (assuming x,y>0) for i in range(itermax):
#program will try to find some a,b,c,d such that 1. Create a vector of random numbers (weights).
#30x^2y^2<=ax^3+by^6 2. Try to find real solution of the problem (with linprog).
#60xy^4<=cx^3+dy^6 3. If there is no solution (status: 2)
#where a+c<=48 and b+d<=56 (assumption 1) 3a. If the solution was never found, break.
#We need some additional equalities to meet assumptions 3b. Else, step back (to the bigger inequality)
#of the weighted AM-GM inequality. 4. If the soltuion was found (status: 0)
#a+b=30 and c+d=60 (assumption 2) Check out which of variables (in example: a,b,c,d) looks like integer.
#3a+0b=30*2, 0a+6b=30*2, 3c+0d=60*1, 0c+6d=60*4 (assumption 3) If there are some inequalities with all integer coefficients, subtract
them from the original one.
#The sketch of the algorithm. If LHS is empty, then break."""
# for i in range(itermax): localseed=shiro.seed
#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=sVars.seed
bufer=[] bufer=[]
lcoef,lfun=_remzero(lcoef,lfun) lcoef,lfun=_remzero(lcoef,lfun)
rcoef,rfun=_remzero(rcoef,rfun) rcoef,rfun=_remzero(rcoef,rfun)
itern=0 itern=0
if len(lcoef)==0: #if LHS is empty if len(lcoef)==0: #if LHS is empty
sVars.display(sVars.translation['status:']+' 0') shiro.display(shiro.translation['status:']+' 0')
status=0 status=0
elif len(rcoef)==0: elif len(rcoef)==0:
#if RHS is empty, but LHS is not #if RHS is empty, but LHS is not
sVars.display(sVars.translation['status:']+' 2') shiro.display(shiro.translation['status:']+' 2')
status=2 status=2
itermax=0 itermax=0
foundreal=0 foundreal=0
@ -208,9 +262,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}) res=linprog(vecc,A_eq=A,b_eq=b,A_ub=A_ub,b_ub=b_ub,options={'maxiter':linprogiter})
status=res.status status=res.status
if itern==1: if itern==1:
sVars.display(sVars.translation['status:']+' '+str(status)) shiro.display(shiro.translation['status:']+' '+str(status))
if status==0: if status==0:
sVars.display(sVars.translation[theorem]) shiro.display(shiro.translation[theorem])
if status==2: #if real solution of current inequality doesn't exist if status==2: #if real solution of current inequality doesn't exist
if foundreal==0: #if this is the first inequality, then break if foundreal==0: #if this is the first inequality, then break
break break
@ -222,7 +276,7 @@ def _list2proof(lcoef,lfun,rcoef,rfun,variables,itermax,linprogiter,_writ2=_writ
continue continue
if status==0:#if found a solution with real coefficients if status==0:#if found a solution with real coefficients
for ineq in bufer: for ineq in bufer:
sVars.display(ineq) shiro.display(ineq)
foundreal=1 foundreal=1
bufer=[] bufer=[]
oldlfun,oldrfun=lfun,rfun oldlfun,oldrfun=lfun,rfun
@ -254,25 +308,25 @@ def _list2proof(lcoef,lfun,rcoef,rfun,variables,itermax,linprogiter,_writ2=_writ
lcoef,lfun=_remzero(lcoef,lfun) lcoef,lfun=_remzero(lcoef,lfun)
rcoef,rfun=_remzero(rcoef,rfun) rcoef,rfun=_remzero(rcoef,rfun)
for ineq in bufer: for ineq in bufer:
sVars.display(ineq) shiro.display(ineq)
lhs='+'.join([_writ2(c,f,variables) for c,f in zip(lcoef,lfun)]) lhs='+'.join([_writ2(c,f,variables) for c,f in zip(lcoef,lfun)])
if lhs=='': if lhs=='':
lhs='0' lhs='0'
elif status==0: elif status==0:
sVars.display(sVars.translation[ shiro.display(shiro.translation[
"Program couldn't find a solution with integer coefficients. Try "+ "Program couldn't find a solution with integer coefficients. Try "+
"to multiple the formula by some integer and run this function again."]) "to multiple the formula by some integer and run this function again."])
elif(status==2): elif(status==2):
sVars.display(sVars.translation["Program couldn't find any proof."]) shiro.display(shiro.translation["Program couldn't find any proof."])
#return res.status #return res.status
elif status==1: elif status==1:
sVars.display(sVars.translation["Try to set higher linprogiter parameter."]) shiro.display(shiro.translation["Try to set higher linprogiter parameter."])
rhs='+'.join([_writ2(c,f,variables) for c,f in zip(rcoef,rfun)]) rhs='+'.join([_writ2(c,f,variables) for c,f in zip(rcoef,rfun)])
if rhs=='': if rhs=='':
rhs='0' rhs='0'
sVars.display('$$ '+slatex(lhs)+' \\le '+slatex(rhs)+' $$') shiro.display('$$ '+latex(lhs)+' \\le '+latex(rhs)+' $$')
if lhs=='0': if lhs=='0':
sVars.display(sVars.translation['The sum of all inequalities gives us a proof of the inequality.']) shiro.display(shiro.translation['The sum of all inequalities gives us a proof of the inequality.'])
return status return status
def _isiterable(obj): def _isiterable(obj):
try: try:
@ -281,18 +335,25 @@ def _isiterable(obj):
except TypeError: except TypeError:
return False return False
def _smakeiterable(x): def _smakeiterable(x):
if x=='':
return []
x=S(x) x=S(x)
if _isiterable(x): if _isiterable(x):
return x return x
return (x,) return (x,)
def _smakeiterable2(x): def _smakeiterable2(x):
if x=='':
return []
x=S(x) x=S(x)
if len(x)==0:
return []
if _isiterable(x[0]): if _isiterable(x[0]):
return x return x
return (x,) return (x,)
def prove(formula,values=None,variables=None,niter=200,linprogiter=10000): def prove(formula,values=None,variables=None,niter=200,linprogiter=10000):
#tries to prove that formula>=0 assuming all variables are positive """tries to prove that formula>=0 assuming all variables are positive"""
formula=S(formula) formula=S(formula)
addsymbols(formula)
if variables: variables=_smakeiterable(variables) if variables: variables=_smakeiterable(variables)
else: variables=sorted(formula.free_symbols,key=str) else: variables=sorted(formula.free_symbols,key=str)
if values: values=_smakeiterable(values) if values: values=_smakeiterable(values)
@ -301,46 +362,50 @@ def prove(formula,values=None,variables=None,niter=200,linprogiter=10000):
st=_list2proof(*(_formula2list(num)+(niter,linprogiter))) st=_list2proof(*(_formula2list(num)+(niter,linprogiter)))
if st==2 and issymetric(num): if st==2 and issymetric(num):
fs=sorted([str(x) for x in num.free_symbols]) fs=sorted([str(x) for x in num.free_symbols])
sVars.display(sVars.translation["It looks like the formula is symmetric. "+ shiro.display(shiro.translation["It looks like the formula is symmetric. "+
"You can assume without loss of generality that "]+ "You can assume without loss of generality that "]+
' >= '.join([str(x) for x in fs])+'. '+sVars.translation['Try']) ' >= '.join([str(x) for x in fs])+'. '+shiro.translation['Try'])
sVars.display('prove(makesubs(S("'+str(num)+'"),'+ shiro.display('prove(makesubs(S("'+str(num)+'"),'+
str([(str(x),'oo') for x in variables[1:]])+')') str([(str(x),'oo') for x in variables[1:]])+')')
return st return st
def powerprove(formula,values=None,variables=None,niter=200,linprogiter=10000): def powerprove(formula,values=None,variables=None,niter=200,linprogiter=10000):
#This is a bruteforce and ineffective function for proving inequalities. """This is a bruteforce and ineffective function for proving inequalities.
#It can be used as the last resort. It can be used as the last resort."""
formula=S(formula) formula=S(formula)
addsymbols(formula)
if variables: variables=_smakeiterable(variables) if variables: variables=_smakeiterable(variables)
else: variables=sorted(formula.free_symbols,key=str) else: variables=sorted(formula.free_symbols,key=str)
if values: values=_smakeiterable(values) if values: values=_smakeiterable(values)
else: values=[1]*len(variables) else: values=[1]*len(variables)
num,den=_input2fraction(formula,variables,values) num,den=_input2fraction(formula,variables,values)
subst2=[]
statusses=[] statusses=[]
for j in range(len(variables)):
subst2+=[(variables[j],1+variables[j])]
for i in range(1<<len(variables)): #tricky substitutions to improve speed for i in range(1<<len(variables)): #tricky substitutions to improve speed
sVars.display('\n\\hline\n') shiro.display(r'_______________________')
subst1=[] subst1=[]
subst2=[]
substout=[] substout=[]
for j in range(len(variables)): for j in range(len(variables)):
z=newvar()
x=variables[j]
subst2+=[(x,1+z)]
if i&(1<<j): if i&(1<<j):
subst1+=[(variables[j],1/variables[j])] subst1+=[(x,1/x)]
substout+=[str(variables[j])+'\\to 1/(1+'+str(variables[j])+')'] substout+=[latex(x)+'\\to 1/(1+'+latex(z)+')']
else: else:
substout+=[str(variables[j])+'\\to 1+'+str(variables[j])] substout+=[latex(x)+'\\to 1+'+latex(z)]
sVars.display(sVars.translation['Substitute']+ ' $'+','.join(substout)+'$') shiro.display(shiro.translation['Substitute']+ ' $'+','.join(substout)+'$')
num1=fractioncancel(num.subs(subst1))[0] num1=fractioncancel(num.subs(subst1))[0]
num2=expand(num1.subs(subst2)) num2=expand(num1.subs(subst2))
sVars.display(sVars.translation["Numerator after substitutions:"]+' $'+slatex(num2)+'$') shiro.display(shiro.translation["Numerator after substitutions:"]+' $'+latex(num2)+'$')
statusses+=[_list2proof(*(_formula2list(num2)+(niter,linprogiter)))] statusses+=[_list2proof(*(_formula2list(num2)+(niter,linprogiter)))]
return Counter(statusses) return Counter(statusses)
def makesubs(formula,intervals,values=None,variables=None,numden=False): def makesubs(formula,intervals,values=None,variables=None,numden=False):
#This function generates a new formula which satisfies this condition: """Generates a new formula which satisfies this condition:
#for all positive variables new formula is nonnegative iff for all positive variables new formula is nonnegative iff
#for all variables in corresponding intervals old formula is nonnegative for all variables in corresponding intervals old formula is nonnegative"""
formula=S(formula) formula=S(formula)
addsymbols(formula)
intervals=_smakeiterable2(intervals) intervals=_smakeiterable2(intervals)
if variables: variables=_smakeiterable(variables) if variables: variables=_smakeiterable(variables)
else: variables=sorted(formula.free_symbols,key=str) else: variables=sorted(formula.free_symbols,key=str)
@ -349,38 +414,45 @@ def makesubs(formula,intervals,values=None,variables=None,numden=False):
equations=[var-value for var,value in zip(variables,values)] equations=[var-value for var,value in zip(variables,values)]
else: else:
equations=[] equations=[]
newvars=[]
warn=0
usedvars=set()
for var,interval in zip(variables,intervals): for var,interval in zip(variables,intervals):
end1,end2=interval end1,end2=interval
z=newvar()
newvars+=[z]
usedvars|={var}
if (end1.free_symbols|end2.free_symbols)&usedvars:
warn=1
if end1 in {S('-oo'),S('oo')}: if end1 in {S('-oo'),S('oo')}:
end1,end2=end2,end1 end1,end2=end2,end1
if {end1,end2}=={S('-oo'),S('oo')}: if {end1,end2}=={S('-oo'),S('oo')}:
formula=formula.subs(var,var-1/var) sub1=sub2=(z-1/z)
equations=[equation.subs(var,var-1/var) for equation in equations]
sVars.display(sVars.translation['Substitute']+' $'+str(var)+'\\to '+sstr(var-1/var)+'$')
elif end2==S('oo'): elif end2==S('oo'):
formula=formula.subs(var,end1+var) sub1=sub2=(end1+z)
equations=[equation.subs(var,end1+var) for equation in equations]
sVars.display(sVars.translation['Substitute']+' $'+str(var)+'\\to '+sstr(end1+var)+'$')
elif end2==S('-oo'): elif end2==S('-oo'):
formula=formula.subs(var,end1-var) sub1=sub2=end1-z
equations=[equation.subs(var,end1-var) for equation in equations]
sVars.display(sVars.translation['Substitute']+" $"+str(var)+'\\to '+sstr(end1-var)+'$')
else: else:
formula=formula.subs(var,end2+(end1-end2)/var) sub1=end2+(end1-end2)/z
sVars.display(sVars.translation['Substitute']+" $"+str(var)+'\\to '+sstr(end2+(end1-end2)/(1+var))+'$') sub2=end2+(end1-end2)/(1+z)
equations=[equation.subs(var,end2+(end1-end2)/var) for equation in equations] formula=formula.subs(var,sub1)
shiro.display(shiro.translation['Substitute']+" $"+latex(var)+'\\to '+latex(sub2)+'$')
equations=[equation.subs(var,sub1) for equation in equations]
num,den=fractioncancel(formula) num,den=fractioncancel(formula)
for var,interval in zip(variables,intervals): for var,interval in zip(newvars,intervals):
if {interval[0],interval[1]} & {S('oo'),S('-oo')}==set(): if {interval[0],interval[1]} & {S('oo'),S('-oo')}==set():
num=num.subs(var,var+1) num=num.subs(var,var+1)
den=den.subs(var,var+1) den=den.subs(var,var+1)
equations=[equation.subs(var,var+1) for equation in equations] equations=[equation.subs(var,var+1) for equation in equations]
if values: if values:
values=ssolve(equations,variables) values=ssolve(equations,newvars)
if len(values): if len(values):
values=values[0] values=values[0]
num,den=expand(num),expand(den) num,den=expand(num),expand(den)
#sVars.display(sVars.translation["Formula after substitution:"],"$$",slatex(num/den),'$$') #shiro.display(shiro.translation["Formula after substitution:"],"$$",latex(num/den),'$$')
if warn:
shiro.warning(shiro.translation[
'Warning: intervals contain backwards dependencies. Consider changing order of variables and intervals.'])
if values and numden: if values and numden:
return num,den,values return num,den,values
elif values: elif values:
@ -390,9 +462,9 @@ def makesubs(formula,intervals,values=None,variables=None,numden=False):
else: else:
return num/den return num/den
def _formula2listf(formula): def _formula2listf(formula):
#Splits a polynomial to a difference of two formulas with positive """Splits a polynomial to a difference of two formulas with positive
#coefficients and extracts coefficients and function coefficients and extracts coefficients and function
#arguments of both formulas. arguments of both formulas."""
lfun=[] lfun=[]
lcoef=[] lcoef=[]
rfun=[] rfun=[]
@ -407,15 +479,19 @@ def _formula2listf(formula):
rfun+=[facts[0].args] rfun+=[facts[0].args]
return(lcoef,lfun,rcoef,rfun,None) return(lcoef,lfun,rcoef,rfun,None)
def provef(formula,niter=200,linprogiter=10000): def provef(formula,niter=200,linprogiter=10000):
#this function is similar to prove, formula is a linear combination of """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 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 is nonnegative for any nonnegative and convex function f. If so, it
#provides a proof of nonnegativity. provides a proof of nonnegativity."""
formula=S(formula) formula=S(formula)
addsymbols(formula)
num,den=_input2fraction(formula,[],[]) num,den=_input2fraction(formula,[],[])
return _list2proof(*(_formula2listf(num)+(niter,linprogiter,_writ,'From Jensen inequality:'))) return _list2proof(*(_formula2listf(num)+(niter,linprogiter,_writ,'From Jensen inequality:')))
def issymetric(formula): #checks if formula is symmetric def issymetric(formula):
#and has at least two variables """checks if formula is symmetric
and has at least two variables"""
formula=S(formula)
addsymbols(formula)
if len(formula.free_symbols)<2: if len(formula.free_symbols)<2:
return False return False
ls=list(formula.free_symbols) ls=list(formula.free_symbols)
@ -425,9 +501,10 @@ def issymetric(formula): #checks if formula is symmetric
return False return False
return True return True
def cyclize(formula,oper=operator.add,variables=None,init=None): 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')=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') cyclize('a^2*b',variables='a,b,c')=S('a^2*b+b^2*c+c^2*a')"""
formula=S(formula) formula=S(formula)
addsymbols(formula)
if variables==None: if variables==None:
variables=sorted(formula.free_symbols,key=str) variables=sorted(formula.free_symbols,key=str)
else: else:
@ -446,10 +523,11 @@ def cyclize(formula,oper=operator.add,variables=None,init=None):
init=oper(init,formula) init=oper(init,formula)
return init return init
def symmetrize(formula,oper=operator.add,variables=None,init=None): 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')=S('a^2*b+b^2*a')
#symmetrize('a^2*b',variables='a,b,c')= 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') =S('a^2*b+a^2*c+b^2*a+b^2*c+c^2*a+c^2*b')"""
formula=S(formula) formula=S(formula)
addsymbols(formula)
if variables==None: if variables==None:
variables=sorted(formula.free_symbols,key=str) variables=sorted(formula.free_symbols,key=str)
else: else:
@ -457,8 +535,10 @@ def symmetrize(formula,oper=operator.add,variables=None,init=None):
for i in range(1,len(variables)): for i in range(1,len(variables)):
formula=cyclize(formula,oper,variables[:i+1]) formula=cyclize(formula,oper,variables[:i+1])
return formula return formula
def findvalues(formula,values=None,variables=None): def findvalues(formula,values=None,variables=None,**kwargs):
"""finds a candidate for parameter "values" in "prove" function"""
formula=S(formula) formula=S(formula)
addsymbols(formula)
num,den=fractioncancel(formula) num,den=fractioncancel(formula)
if variables==None: if variables==None:
variables=sorted(num.free_symbols,key=str) variables=sorted(num.free_symbols,key=str)
@ -471,5 +551,5 @@ def findvalues(formula,values=None,variables=None):
values=[1.0]*len(variables) values=[1.0]*len(variables)
else: else:
values=S(values) values=S(values)
tup=tuple(fmin(f2,values)) tup=tuple(fmin(f2,values,**kwargs))
return tuple([x*x for x in tup]) return tuple([x*x for x in tup])

1563
statistics.ipynb Normal file
View File

File diff suppressed because one or more lines are too long

BIN
statistics.pdf Normal file
View File

Binary file not shown.