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

added a sentence

Browse Source
This commit is contained in:
urojony 2020-04-21 10:13:02 +02:00
parent e7367cf50f
commit e145a4db9f
5 changed files with 1360 additions and 155 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
.ipynb_checkpoints/Untitled-checkpoint.ipynb Normal file
View File

@ -0,0 +1,6 @@
{
"cells": [],
"metadata": {},
"nbformat": 4,
"nbformat_minor": 2
}

1070
Untitled.ipynb Normal file
View File

File diff suppressed because it is too large Load Diff

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

Binary file not shown.

401
examples.ipynb
View File

@ -1,5 +1,12 @@
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"In this notebook there are presented examples of usage of shiroin, a python library for proving inequalities of multivariate polynomials."
]
},
{
"cell_type": "code",
"execution_count": 1,
@ -16,7 +23,7 @@
"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. The next two lines\n",
"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 a slightly different proof each time you run a function. The next two lines provide a nicer display of proofs, i.e. formulas will be shown instead of LaTeX code of these formulas. Note that this works on Jupyter, but not on the git page.\n",
"\n",
"Now let's make some proofs. We will use problems from https://www.imomath.com/index.php?options=593&lmm=0."
]
@ -89,16 +96,6 @@
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
@ -208,7 +205,31 @@
{
"data": {
"text/latex": [
"$$2ab \\le a^2+b^2$$$$2ac \\le a^2+c^2$$$$2bc \\le b^2+c^2$$"
"$$2ab \\le a^2+b^2$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$$2ac \\le a^2+c^2$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$$2bc \\le b^2+c^2$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"
@ -312,16 +333,6 @@
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
@ -436,7 +447,31 @@
{
"data": {
"text/latex": [
"$$2ab \\le a^2+b^2$$$$2ac \\le a^2+c^2$$$$2ad \\le a^2+d^2$$"
"$$2ab \\le a^2+b^2$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$$2ac \\le a^2+c^2$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$$2ad \\le a^2+d^2$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"
@ -559,7 +594,31 @@
{
"data": {
"text/latex": [
"$$28ab \\le 14a^2+14b^2$$$$28ac \\le 14a^2+14c^2$$$$28ad \\le 14a^2+14d^2$$"
"$$28ab \\le 14a^2+14b^2$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$$28ac \\le 14a^2+14c^2$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$$28ad \\le 14a^2+14d^2$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"
@ -661,16 +720,6 @@
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
@ -710,7 +759,7 @@
{
"data": {
"text/latex": [
"prove(makesubs(S(\"-x**3*y + 2*x**2*y**2 - x**2 - x*y**3 + 2*x*y - y**2\"),[('y', 'inf')])"
"prove(makesubs(S(\"-x**3*y + 2*x**2*y**2 - x**2 - x*y**3 + 2*x*y - y**2\"),[('y', 'oo')])"
],
"text/plain": [
"<IPython.core.display.Latex object>"
@ -824,7 +873,43 @@
{
"data": {
"text/latex": [
"$$12x^2y^2 \\le 6x^3y+6xy^3$$$$3x^2y \\le 2x^3+y^3$$$$3xy^2 \\le x^3+2y^3$$$$6xy \\le 3x^2+3y^2$$"
"$$12x^2y^2 \\le 6x^3y+6xy^3$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$$3x^2y \\le 2x^3+y^3$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$$3xy^2 \\le x^3+2y^3$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$$6xy \\le 3x^2+3y^2$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"
@ -984,7 +1069,31 @@
{
"data": {
"text/latex": [
"$$2x^3y \\le x^4y^2+x^2$$$$4x^2y \\le x^3y^2+2x^2+xy^2$$$$2xy \\le x^2+y^2$$"
"$$2x^3y \\le x^4y^2+x^2$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$$4x^2y \\le x^3y^2+2x^2+xy^2$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$$2xy \\le x^2+y^2$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"
@ -1101,7 +1210,31 @@
{
"data": {
"text/latex": [
"$$2ab \\le a^2+b^2$$$$2ac \\le a^2+c^2$$$$2bc \\le b^2+c^2$$"
"$$2ab \\le a^2+b^2$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$$2ac \\le a^2+c^2$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$$2bc \\le b^2+c^2$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"
@ -1201,16 +1334,6 @@
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
@ -1310,16 +1433,6 @@
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
@ -1356,7 +1469,7 @@
}
],
"source": [
"prove(makesubs('(x-1)^4','(1,inf)'))"
"prove(makesubs('(x-1)^4','(1,oo)'))"
]
},
{
@ -1414,16 +1527,6 @@
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
@ -1460,7 +1563,7 @@
}
],
"source": [
"prove(makesubs('(x-1)^4','(-inf,1)'))"
"prove(makesubs('(x-1)^4','(-oo,1)'))"
]
},
{
@ -1540,16 +1643,6 @@
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
@ -1673,16 +1766,6 @@
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
@ -1719,7 +1802,7 @@
}
],
"source": [
"prove(makesubs(formula,'[c,inf],[d,inf]'))"
"prove(makesubs(formula,'[c,oo],[d,oo]'))"
]
},
{
@ -1847,7 +1930,7 @@
}
],
"source": [
"prove(makesubs(formula,'[c,inf],[d,inf]')*2)"
"prove(makesubs(formula,'[c,oo],[d,oo]')*2)"
]
},
{
@ -1937,7 +2020,19 @@
{
"data": {
"text/latex": [
"$$2a^2b^2c^3d \\le a^3bc^2d^2+ab^3c^4$$$$2a^2c^3d \\le a^3c^2d^2+ac^4$$"
"$$2a^2b^2c^3d \\le a^3bc^2d^2+ab^3c^4$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$$2a^2c^3d \\le a^3c^2d^2+ac^4$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"
@ -2082,16 +2177,6 @@
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
@ -2165,16 +2250,6 @@
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
@ -2379,16 +2454,6 @@
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
@ -2574,7 +2639,19 @@
{
"data": {
"text/latex": [
"$$2ab \\le a^2+b^2$$$$2bc \\le b^2+c^2$$"
"$$2ab \\le a^2+b^2$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$$2bc \\le b^2+c^2$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"
@ -2683,7 +2760,31 @@
{
"data": {
"text/latex": [
"$$2abc^3 \\le a^2bc^3+bc^3$$$$2ab \\le a^2+b^2$$$$2bc \\le b^2+c^2$$"
"$$2abc^3 \\le a^2bc^3+bc^3$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$$2ab \\le a^2+b^2$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$$2bc \\le b^2+c^2$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"
@ -2804,7 +2905,19 @@
{
"data": {
"text/latex": [
"$$4abc \\le a^2c^2+2ab^2+c^2$$$$2bc \\le b^2+c^2$$"
"$$4abc \\le a^2c^2+2ab^2+c^2$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$$2bc \\le b^2+c^2$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"
@ -2886,16 +2999,6 @@
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
@ -3091,7 +3194,31 @@
{
"data": {
"text/latex": [
"$$21f(1, 2, 3) \\le 11f(-1, 4, 3)+8f(3, -1, 4)+2f(4, 3, -1)$$$$21f(2, 3, 1) \\le 8f(-1, 4, 3)+2f(3, -1, 4)+11f(4, 3, -1)$$$$21f(3, 1, 2) \\le 2f(-1, 4, 3)+11f(3, -1, 4)+8f(4, 3, -1)$$"
"$$21f(1, 2, 3) \\le 11f(-1, 4, 3)+8f(3, -1, 4)+2f(4, 3, -1)$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$$21f(2, 3, 1) \\le 8f(-1, 4, 3)+2f(3, -1, 4)+11f(4, 3, -1)$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$$21f(3, 1, 2) \\le 2f(-1, 4, 3)+11f(3, -1, 4)+8f(4, 3, -1)$$"
],
"text/plain": [
"<IPython.core.display.Latex object>"

38
shiroindev.py
View File

@ -26,7 +26,7 @@ for phrase in translationList:
sVars.translation[phrase]=phrase
from scipy.optimize import linprog
import random
from sympy import S,cancel,fraction,Pow,expand,solve,latex
from sympy import S,cancel,fraction,Pow,expand,solve,latex,oo
import re
def _remzero(coef,fun):
#coef, fun represents an expression.
@ -76,7 +76,7 @@ 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(' ','')
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)
@ -156,7 +156,7 @@ def _list2proof(lcoef,lfun,rcoef,rfun,variables,itermax,linprogiter,_writ2=_writ
#them from the original one.
#If LHS is empty, then break.
localseed=sVars.seed
bufer=''
bufer=[]
itern=0
if len(lcoef)==0: #if LHS is empty
sVars.print(sVars.translation['status:']+' 0')
@ -210,13 +210,13 @@ def _list2proof(lcoef,lfun,rcoef,rfun,variables,itermax,linprogiter,_writ2=_writ
#step back
lcoef,lfun=oldlcoef,oldlfun
rcoef,rfun=oldrcoef,oldrfun
bufer=''
bufer=[]
continue
if status==0:#if found a solution with real coefficients
if bufer:
sVars.print(bufer)
for ineq in bufer:
sVars.print(ineq)
foundreal=1
bufer=''
bufer=[]
oldlfun,oldrfun=lfun,rfun
oldlcoef,oldrcoef=lcoef[:],rcoef[:]
for i in range(m):
@ -231,20 +231,22 @@ def _list2proof(lcoef,lfun,rcoef,rfun,variables,itermax,linprogiter,_writ2=_writ
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 '
bufer+=['']
bufer[-1]+='$$'+_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+='+'
if(c):bufer[-1]+='+'
else:c=1
bufer+=_writ2(int(round(j)),k,variables)
bufer+='$$'
bufer[-1]+=_writ2(int(round(j)),k,variables)
bufer[-1]+='$$'
lcoef,lfun=_remzero(lcoef,lfun)
rcoef,rfun=_remzero(rcoef,rfun)
sVars.print(bufer)
for ineq in bufer:
sVars.print(ineq)
lhs='+'.join([_writ2(c,f,variables) for c,f in zip(lcoef,lfun)])
if lhs=='':
lhs='0'
@ -295,7 +297,7 @@ def prove(formula,values=None,variables=None,niter=200,linprogiter=10000):
"You can assume without loss of generality that "]+
' >= '.join([str(x) for x in fs])+'. '+sVars.translation['Try'])
sVars.print('prove(makesubs(S("'+str(num)+'"),'+
str([(str(x),'inf') for x in variables[1:]])+')')
str([(str(x),'oo') 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.
@ -339,17 +341,17 @@ def makesubs(formula,intervals,values=None,variables=None,numden=False):
equations=[]
for var,interval in zip(variables,intervals):
end1,end2=interval
if end1 in {S('-inf'),S('inf')}:
if end1 in {S('-oo'),S('oo')}:
end1,end2=end2,end1
if {end1,end2}=={S('-inf'),S('inf')}:
if {end1,end2}=={S('-oo'),S('oo')}:
formula=formula.subs(var,var-1/var)
equations=[equation.subs(var,var-1/var) for equation in equations]
sVars.print(sVars.translation['Substitute']+' $'+str(var)+'\\to '+var-1/var+'$')
elif end2==S('inf'):
elif end2==S('oo'):
formula=formula.subs(var,end1+var)
equations=[equation.subs(var,end1+var) for equation in equations]
sVars.print(sVars.translation['Substitute']+' $'+str(var)+'\\to '+sstr(end1+var)+'$')
elif end2==S('-inf'):
elif end2==S('-oo'):
formula=formula.subs(var,end1-var)
equations=[equation.subs(var,end1-var) for equation in equations]
sVars.print(sVars.translation['Substitute']+" $"+str(var)+'\\to '+sstr(end1-var)+'$')
@ -359,7 +361,7 @@ def makesubs(formula,intervals,values=None,variables=None,numden=False):
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():
if {interval[0],interval[1]} & {S('oo'),S('-oo')}==set():
num=num.subs(var,var+1)
den=den.subs(var,var+1)
equations=[equation.subs(var,var+1) for equation in equations]