diff --git a/.ipynb_checkpoints/Untitled-checkpoint.ipynb b/.ipynb_checkpoints/Untitled-checkpoint.ipynb new file mode 100644 index 0000000..2fd6442 --- /dev/null +++ b/.ipynb_checkpoints/Untitled-checkpoint.ipynb @@ -0,0 +1,6 @@ +{ + "cells": [], + "metadata": {}, + "nbformat": 4, + "nbformat_minor": 2 +} diff --git a/Untitled.ipynb b/Untitled.ipynb new file mode 100644 index 0000000..dca4f4c --- /dev/null +++ b/Untitled.ipynb @@ -0,0 +1,1070 @@ +{ + "cells": [ + { + "cell_type": "code", + "execution_count": 1, + "metadata": {}, + "outputs": [], + "source": [ + "def extrema(fr):\n", + " t=[]\n", + " for x in fr.free_symbols:\n", + " t+=[fr.diff(x)]\n", + " print(t)\n", + " return solve(t)" + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "metadata": {}, + "outputs": [], + "source": [ + "from shiroindev import *\n", + "from itertools import permutations, combinations\n", + "sVars.seed=1\n", + "from IPython.display import Latex\n", + "sVars.print=lambda x:display(Latex(x))" + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "metadata": {}, + "outputs": [ + { + "data": { + "text/latex": [ + "numerator: $12a^3-18a^2b+6a^2c+6ab^2-18ac^2+12b^3-18b^2c+6bc^2+12c^3$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "denominator: $4a^2b+2a^2c+2ab^2+9abc+4ac^2+4b^2c+2bc^2$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "status: 0" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "From weighted AM-GM inequality:" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$18a^2b \\le 10a^3+6ab^2+2b^3$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$18ac^2 \\le 2a^3+6a^2c+10c^3$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$18b^2c \\le 10b^3+6bc^2+2c^3$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$ 0 \\le 0 $$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "The sum of all inequalities gives us a proof of the inequality." + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/plain": [ + "0" + ] + }, + "execution_count": 3, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "formula=cyclize('(a+b)/(2*b+c)')-2\n", + "prove(formula*6)" + ] + }, + { + "cell_type": "code", + "execution_count": 63, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "a**2 - a*(b + c + d) + b**2 + c**2 + d**2\n", + "[-a*(1 - 1/(a*b**2*c)) + 2*b - 2/(a**2*b**3*c**2), -a*(1 - 1/(a*b*c**2)) + 2*c - 2/(a**2*b**2*c**3), 2*a - b - c - 2/(a**3*b**2*c**2)]\n" + ] + } + ], + "source": [ + "point(Sm('(a^2+b^2+c^2+d^2)-a*(b+c+d)'))" + ] + }, + { + "cell_type": "code", + "execution_count": 5, + "metadata": {}, + "outputs": [ + { + "data": { + "text/latex": [ + "Substitute $a\\to s-s/(a+1)$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Substitute $b\\to s-s/(b+1)$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Substitute $c\\to s-s/(c+1)$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "numerator: $abcs^2+s^2$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "denominator: $abc+ab+ac+a+bc+b+c+1$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "status: 0" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$ 0 \\le abcs^2+s^2 $$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "The sum of all inequalities gives us a proof of the inequality." + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/plain": [ + "0" + ] + }, + "execution_count": 5, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "prove(makesubs(Sm('-a(s-b)-b(s-c)-c(s-a)+ s^2'),'[0,s],[0,s],[0,s]'))" + ] + }, + { + "cell_type": "code", + "execution_count": 6, + "metadata": {}, + "outputs": [], + "source": [ + "def nonneg(formula):\n", + " formula=expand(formula)\n", + " for addend in formula.as_ordered_terms():\n", + " coef,facts=addend.as_coeff_mul()\n", + " if coef<0:\n", + " return False\n", + " return True" + ] + }, + { + "cell_type": "code", + "execution_count": 7, + "metadata": {}, + "outputs": [ + { + "data": { + "text/latex": [ + "$\\displaystyle \\infty$" + ], + "text/plain": [ + "oo" + ] + }, + "execution_count": 7, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "oo" + ] + }, + { + "cell_type": "code", + "execution_count": 8, + "metadata": {}, + "outputs": [], + "source": [ + "def symprove(formula,n):\n", + " formula=S(formula)\n", + " if n==0:\n", + " return\n", + " ls=list(formula.free_symbols)\n", + " for i in range(len(ls)):\n", + " a=ls[i]\n", + " for j in range(i+1,len(ls)):\n", + " b=ls[j]\n", + " if expand(formula-formula.subs({a:b, b:a}, simultaneous=True))==S(0):\n", + " formula=makesubs(formula,[[b,S('oo')]],variables=[a,b])\n", + " sVars.print('$$'+latex(formula)+'$$')\n", + " symprove(formula,n-1)" + ] + }, + { + "cell_type": "code", + "execution_count": 9, + "metadata": {}, + "outputs": [ + { + "data": { + "text/latex": [ + "Substitute $x\\to x+y$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$x^{2}$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "symprove('x^2-2*x*y+y^2',4)" + ] + }, + { + "cell_type": "code", + "execution_count": 45, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "(y, x)\n" + ] + }, + { + "data": { + "text/latex": [ + "Substitute $x\\to x+y$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$x^{2} \\left(x + y\\right)^{t} - x y y^{t} + x y z^{t} + x y \\left(x + y\\right)^{t} + x y^{t} z - x z z^{t} - x z \\left(x + y\\right)^{t} + y^{2} z^{t} - 2 y z z^{t} + z^{2} z^{t}$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "(y, x)\n", + "(y, t)\n", + "(x, t)\n", + "(y, x, t)\n", + "(y, t)\n", + "(x, t)\n", + "(y, x, t)\n" + ] + } + ], + "source": [ + "provesym(Sm('x^t(x-y)(x-z) + y^t (y-z)(y-x) + z^t (z-x)(z-y)'),4)" + ] + }, + { + "cell_type": "code", + "execution_count": 11, + "metadata": {}, + "outputs": [ + { + "data": { + "text/latex": [ + "Substitute $x\\to x+y$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$\\displaystyle x^{2} \\left(x + y\\right)^{t} - x y y^{t} + x y z^{t} + x y \\left(x + y\\right)^{t} + x y^{t} z - x z z^{t} - x z \\left(x + y\\right)^{t} + y^{2} z^{t} - 2 y z z^{t} + z^{2} z^{t}$" + ], + "text/plain": [ + "x**2*(x + y)**t - x*y*y**t + x*y*z**t + x*y*(x + y)**t + x*y**t*z - x*z*z**t - x*z*(x + y)**t + y**2*z**t - 2*y*z*z**t + z**2*z**t" + ] + }, + "execution_count": 11, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "makesubs(Sm('x^t(x-y)(x-z) + y^t (y-z)(y-x) + z^t (z-x)(z-y)'),'[y,oo]',variables='x')" + ] + }, + { + "cell_type": "code", + "execution_count": 12, + "metadata": {}, + "outputs": [ + { + "data": { + "text/latex": [ + "Substitute $x\\to x+y$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$\\displaystyle x^{2} \\left(x + y\\right)^{t} - x y y^{t} + x y z^{t} + x y \\left(x + y\\right)^{t} + x y^{t} z - x z z^{t} - x z \\left(x + y\\right)^{t} + y^{2} z^{t} - 2 y z z^{t} + z^{2} z^{t}$" + ], + "text/plain": [ + "x**2*(x + y)**t - x*y*y**t + x*y*z**t + x*y*(x + y)**t + x*y**t*z - x*z*z**t - x*z*(x + y)**t + y**2*z**t - 2*y*z*z**t + z**2*z**t" + ] + }, + "execution_count": 12, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "makesubs(Sm('x^t*(x-y)(x-z) + y^t*(y-z)(y-x) + z^t*(z-x)(z-y)'),'[y,oo]',variables='x')" + ] + }, + { + "cell_type": "code", + "execution_count": 56, + "metadata": {}, + "outputs": [], + "source": [ + "def provesym(formula,n):\n", + " formula=S(formula)\n", + " if n==0:\n", + " return\n", + " fs=list(formula.free_symbols)\n", + " print \n", + " for i in range(2,len(fs)+1):\n", + " for fs2 in combinations(fs,i):\n", + " for fsp in permutations(fs2[1:]):\n", + " if expand(formula-formula.subs(zip((fs2[0],)+fsp,fsp+(fs2[0],)), simultaneous=True))==S(0):\n", + " newformula=makesubs(formula,[[fs2[0],oo]]*(len(fsp)),variables=fsp)\n", + " sVars.print(str(n)+' $$'+latex(newformula)+'$$')\n", + " provesym(newformula,n-1)" + ] + }, + { + "cell_type": "code", + "execution_count": 57, + "metadata": {}, + "outputs": [ + { + "data": { + "text/latex": [ + "Substitute $y\\to y+z$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "4 $$x^{2} x^{t} - x x^{t} y - 2 x x^{t} z + x y z^{t} - x y \\left(y + z\\right)^{t} + x^{t} y z + x^{t} z^{2} + y^{2} \\left(y + z\\right)^{t} - y z z^{t} + y z \\left(y + z\\right)^{t}$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Substitute $x\\to x+z$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "4 $$x^{2} \\left(x + z\\right)^{t} - x y y^{t} + x y z^{t} - x y \\left(x + z\\right)^{t} + x y^{t} z - x z z^{t} + x z \\left(x + z\\right)^{t} + y^{2} y^{t} - 2 y y^{t} z + y^{t} z^{2}$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Substitute $x\\to x+y$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "4 $$x^{2} \\left(x + y\\right)^{t} - x y y^{t} + x y z^{t} + x y \\left(x + y\\right)^{t} + x y^{t} z - x z z^{t} - x z \\left(x + y\\right)^{t} + y^{2} z^{t} - 2 y z z^{t} + z^{2} z^{t}$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Substitute $y\\to y+z$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Substitute $x\\to x+z$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "4 $$x^{2} \\left(x + z\\right)^{t} + x y z^{t} - x y \\left(x + z\\right)^{t} - x y \\left(y + z\\right)^{t} + y^{2} \\left(y + z\\right)^{t}$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Substitute $x\\to x+y$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "3 $$x^{2} \\left(x + y + z\\right)^{t} + x y z^{t} - x y \\left(y + z\\right)^{t} + x y \\left(x + y + z\\right)^{t} + y^{2} z^{t}$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Substitute $x\\to x+z$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Substitute $y\\to y+z$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "4 $$x^{2} \\left(x + z\\right)^{t} + x y z^{t} - x y \\left(x + z\\right)^{t} - x y \\left(y + z\\right)^{t} + y^{2} \\left(y + z\\right)^{t}$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Substitute $x\\to x+y$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "3 $$x^{2} \\left(x + y + z\\right)^{t} + x y z^{t} - x y \\left(y + z\\right)^{t} + x y \\left(x + y + z\\right)^{t} + y^{2} z^{t}$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "provesym(Sm('x^t(x-y)(x-z) + y^t (y-z)(y-x) + z^t (z-x)(z-y)'),4)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Sm('x^t(x-y)(x-z) + y^t (y-z)(y-x) + z^t (z-x)(z-y)')" + ] + }, + { + "cell_type": "code", + "execution_count": 16, + "metadata": {}, + "outputs": [ + { + "data": { + "text/latex": [ + "$\\displaystyle 3 x + y + 2 z$" + ], + "text/plain": [ + "3*x + y + 2*z" + ] + }, + "execution_count": 16, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "S('x+2*y+3*z').subs(zip(S('[x,y,z]'),S('[y,z,x]')),simultaneous=True)" + ] + }, + { + "cell_type": "code", + "execution_count": 15, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "[x, y, z]" + ] + }, + "execution_count": 15, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "S('[x,y,z]')" + ] + }, + { + "cell_type": "code", + "execution_count": 37, + "metadata": {}, + "outputs": [ + { + "data": { + "text/latex": [ + "$\\displaystyle - t x y^{2} + t x z^{2} - x^{2} \\left(x + y\\right)^{t} + x^{2} \\left(x + z\\right)^{t} + x y y^{t} - x y \\left(x + y\\right)^{t} - x y \\left(x + z\\right)^{t} - x z z^{t} + x z \\left(x + y\\right)^{t} + x z \\left(x + z\\right)^{t} + y^{2} y^{t} - y^{2} z^{t} - 2 y y^{t} z + 2 y z z^{t} + y^{t} z^{2} - z^{2} z^{t}$" + ], + "text/plain": [ + "-t*x*y**2 + t*x*z**2 - x**2*(x + y)**t + x**2*(x + z)**t + x*y*y**t - x*y*(x + y)**t - x*y*(x + z)**t - x*z*z**t + x*z*(x + y)**t + x*z*(x + z)**t + y**2*y**t - y**2*z**t - 2*y*y**t*z + 2*y*z*z**t + y**t*z**2 - z**2*z**t" + ] + }, + "execution_count": 37, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "formula=Sm('x^2(x+y)^t-xyy^t+xyz^t+xy(x+y)^t+xy^tz-xzzt-xz(x+y)^t+y^2z^t-2yzz^t+z^2z^t')\n", + "expand(formula.subs(S('[y,z],[z,y]'),simultaneous=True)-formula)" + ] + }, + { + "cell_type": "code", + "execution_count": 71, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "a**2 - a*(b + c + 1/(a*b*c)) + b**2 + c**2 + 1/(a**2*b**2*c**2)\n", + "[-a*(1 - 1/(a*b**2*c)) + 2*b - 2/(a**2*b**3*c**2), -a*(1 - 1/(a*b*c**2)) + 2*c - 2/(a**2*b**2*c**3), 2*a - b - c - 2/(a**3*b**2*c**2)]\n" + ] + }, + { + "data": { + "text/plain": [ + "[]" + ] + }, + "execution_count": 71, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "def point(formula):\n", + " fs=list(formula.free_symbols)\n", + " il=1\n", + " for s in fs[1:]:\n", + " il*=s\n", + " fr=formula.subs(fs[0],1/il)\n", + " print(fr)\n", + " return(extrema(fr))\n", + "point(Sm('(a^2+b^2+c^2+d^2)-a*(b+c+d)'))" + ] + }, + { + "cell_type": "code", + "execution_count": 69, + "metadata": {}, + "outputs": [ + { + "data": { + "text/latex": [ + "Substitute $a\\to 343a/216$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Substitute $b\\to 6b/7$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Substitute $c\\to 6c/7$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Substitute $d\\to 6d/7$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "numerator: $5764801a^2-3111696ab-3111696ac-3111696ad+1679616b^2+1679616c^2+1679616d^2$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "denominator: $2286144$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "status: 0" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "From weighted AM-GM inequality:" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$3111696ab \\le 1555848a^2+1555848b^2$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$3111696ac \\le 1555848a^2+1555848c^2$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$3111696ad \\le 1555848a^2+1555848d^2$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$ 0 \\le 1097257a^2+123768b^2+123768c^2+123768d^2 $$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "The sum of all inequalities gives us a proof of the inequality." + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/plain": [ + "0" + ] + }, + "execution_count": 69, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "prove(Sm('(a^2+b^2+c^2+d^2)-a*(b+c+d)'),'343/216,6/7,6/7,6/7')" + ] + }, + { + "cell_type": "code", + "execution_count": 68, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "23/375" + ] + }, + "execution_count": 68, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "216/125-5/3" + ] + }, + { + "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 +} diff --git a/__pycache__/shiroindev.cpython-37.pyc b/__pycache__/shiroindev.cpython-37.pyc index ac4b1c5..e8efac0 100644 Binary files a/__pycache__/shiroindev.cpython-37.pyc and b/__pycache__/shiroindev.cpython-37.pyc differ diff --git a/examples.ipynb b/examples.ipynb index 4df967b..ecc0aa6 100644 --- a/examples.ipynb +++ b/examples.ipynb @@ -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": [ - "" - ] - }, - "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": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$2ac \\le a^2+c^2$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$2bc \\le b^2+c^2$$" ], "text/plain": [ "" @@ -312,16 +333,6 @@ "metadata": {}, "output_type": "display_data" }, - { - "data": { - "text/latex": [], - "text/plain": [ - "" - ] - }, - "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": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$2ac \\le a^2+c^2$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$2ad \\le a^2+d^2$$" ], "text/plain": [ "" @@ -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": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$28ac \\le 14a^2+14c^2$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$28ad \\le 14a^2+14d^2$$" ], "text/plain": [ "" @@ -661,16 +720,6 @@ "metadata": {}, "output_type": "display_data" }, - { - "data": { - "text/latex": [], - "text/plain": [ - "" - ] - }, - "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": [ "" @@ -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": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$3x^2y \\le 2x^3+y^3$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$3xy^2 \\le x^3+2y^3$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$6xy \\le 3x^2+3y^2$$" ], "text/plain": [ "" @@ -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": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$4x^2y \\le x^3y^2+2x^2+xy^2$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$2xy \\le x^2+y^2$$" ], "text/plain": [ "" @@ -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": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$2ac \\le a^2+c^2$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$2bc \\le b^2+c^2$$" ], "text/plain": [ "" @@ -1201,16 +1334,6 @@ "metadata": {}, "output_type": "display_data" }, - { - "data": { - "text/latex": [], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, { "data": { "text/latex": [ @@ -1310,16 +1433,6 @@ "metadata": {}, "output_type": "display_data" }, - { - "data": { - "text/latex": [], - "text/plain": [ - "" - ] - }, - "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": [ - "" - ] - }, - "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": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, { "data": { "text/latex": [ @@ -1673,16 +1766,6 @@ "metadata": {}, "output_type": "display_data" }, - { - "data": { - "text/latex": [], - "text/plain": [ - "" - ] - }, - "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": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$2a^2c^3d \\le a^3c^2d^2+ac^4$$" ], "text/plain": [ "" @@ -2082,16 +2177,6 @@ "metadata": {}, "output_type": "display_data" }, - { - "data": { - "text/latex": [], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, { "data": { "text/latex": [ @@ -2165,16 +2250,6 @@ "metadata": {}, "output_type": "display_data" }, - { - "data": { - "text/latex": [], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, { "data": { "text/latex": [ @@ -2379,16 +2454,6 @@ "metadata": {}, "output_type": "display_data" }, - { - "data": { - "text/latex": [], - "text/plain": [ - "" - ] - }, - "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": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$2bc \\le b^2+c^2$$" ], "text/plain": [ "" @@ -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": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$2ab \\le a^2+b^2$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$2bc \\le b^2+c^2$$" ], "text/plain": [ "" @@ -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": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$2bc \\le b^2+c^2$$" ], "text/plain": [ "" @@ -2886,16 +2999,6 @@ "metadata": {}, "output_type": "display_data" }, - { - "data": { - "text/latex": [], - "text/plain": [ - "" - ] - }, - "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": [ + "" + ] + }, + "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": [ + "" + ] + }, + "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": [ "" diff --git a/shiroindev.py b/shiroindev.py index 1c21cea..873b512 100644 --- a/shiroindev.py +++ b/shiroindev.py @@ -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]