From e145a4db9f9d184841368260604c4828e1ecdfd1 Mon Sep 17 00:00:00 2001 From: urojony Date: Tue, 21 Apr 2020 10:13:02 +0200 Subject: [PATCH] added a sentence --- .ipynb_checkpoints/Untitled-checkpoint.ipynb | 6 + Untitled.ipynb | 1070 ++++++++++++++++++ __pycache__/shiroindev.cpython-37.pyc | Bin 13936 -> 14026 bytes examples.ipynb | 401 ++++--- shiroindev.py | 38 +- 5 files changed, 1360 insertions(+), 155 deletions(-) create mode 100644 .ipynb_checkpoints/Untitled-checkpoint.ipynb create mode 100644 Untitled.ipynb 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 ac4b1c532075c55ce8a27a9344ffbd49999b418a..e8efac06edeb200ef97c94c0429adf4127cc1b9f 100644 GIT binary patch delta 4151 zcma)9YiwM_6~1%#-s|i2?%G~^z22w2yMC>o>sOo*hlG%rJitjvN`hk`#m*I@ViKoKLK9dRq(V@excvdDDphKvszQkJ1F0%PLY4ZXT$O^TC@p;mscI$Ks_i** z{Q|pEZQV07XTEc0=A1L<%zl=Ad)B?%?RHA=_r#kwA3gV+J3wB0uJz{&v%#?-k*GxF zY-lV*>!|;-G!~}yGyrXc25AV|C=JsHv<);$8=!5ZjWh;rjK*mK+Bj{Z&Cn)j3vGqA ziMG)sw9T}gc0k)gJ82iRt?4LrP06&I_FN`oZ8Sv}dV!s!eY79ib~-=@q3xji=~lW8 zAf5C8y^C&#UKc$`chI|`*G+fQU4ZJL_tSgmZs4Toy>t(7dehqJJ}Ogr%0c(i5t!*; z$GMO01I_@Ik4ni0{(zQ9D%PD(iS8ge|ErQxEIFU&3H1#U;UB4gCoTLv?N9L*z_BVM zNg$STI-kk0dK7lB0J4Mpld@it;sO0+AclO|Mmn-rm7I|_C1dlEII zi@#8wj@b;9B(}y1M7WT20ofw)-*ndTlrtL^$W9yCf%EH-{3p&G2?UI(Y-&E25p$qX z;8v9l*~)Ik+B}w{Fh2{MUE5C+F1HoFf(%5%li)$w5Rhcq%4uJ&Xd(grW<{I~^WRoH zN}Bm@SCZ`FS=SiZ!GGq80Ow=ZFxkuF?rWr-|G*uAgTC$FL>uy3ku)HQBEq&LYr;NZ&HNQl6FJD=@${48^Oe0CVpszos_bgphh21#09z`X z$W5nN92p5D=s-}{%&%AWkVE|S%D<6b{-dfPQqMoFY8Vuf!qdAEy%*6sTivgvot?2CDPgMzu-DID^)@x_!tNlDq-UKfB@5oM)a+zF zJ;k>1&%6;IhLNRCO-vdEOFNT4mu3Yv!s9h37ban5vK$Ehp&6X;Ip8b2ph}Vq*!6drnE>XnUUFmA>DSstU~30L>+!%R@O?j(li;8ie9tY^amuw~@XLq*_xKt&plSum1E^ZibI{k3(P{Z*$jaGS10Vjtgx!}AY(f#a&c zUN_xnP>^DWrCiVqnju*#N=0IZ%?R}5q65u8M^O$8PtVtz&OOp2RmCW-Vn)&MC3)`V zafxb0_q4?K)+PPd@f3K15_#mwVjY;ep+wG~;qTVf^KaMr+@2Yw%y8t8U_#ZfPY8X_m4~G&l_c+F0>%SW{!=^ zMSn47`l&~_&I@Y)Wj25l+gDUj?+}F5u#{6^n++@6tCHb0s!abPStMrcDp_>cD3m`g zt)OVtG8Z;?Trz4*$s~(1tO;h~ANaiso7zN~D}hbCw`;FRR|r&u8t|@el-a`Q+a*$r zn{iqR)>qgsX>Bo{d(gHrj6YlTAzU7`ac&FDq0dz2TAiyCbNp1jR)(%uSqq=7k1W^= z$);lwtRogmmhR=*+SkP(+5uce5{orz##A&V2SXx~yWN*ZDL3Ig_ zG6I+MLRrC>Fy;$)U6317@b$6#fm_CUfwDgSY^;?J2f}ti7+o$1EHL54yf)o+Z}^WN zZ3*ra>5zXIIMOZ>bqHm{Kp>l?u)ms5*DA(8?wkz9$^Vbn_$#3ksUx7xQVQubW&No5 zK_o{7Gn*+GmSc9}%(@&$c~3aFM_Et1*cBvnL#e3ViGmf4E_{ehGM3WBK zcjBjf%x`aJgM0+#J8@;Zu(KEfJ@&I^kfZW;lI zrHWUA{V2m1&f1MU%C~kTHAh!I&-}b9;Nyp*3cuLV*^f4W0K$zfd)(5~bMq5MCZ7X7 zs$KucgW)*;upUHcX`p3UCmrpL;!MQ5_w4$RBAsm4FLJf#yMqrSW(>(rAS>@ik>y0b6Io8=yGId(uRZn{|8-BCJjwsl6C*G2SnAwE zYuD~21Pq`m)xKMs1m~B644#cFe>Oe!ELu?mQAyPy5we^7FR5#XvFeP7iX`sbu_Uov zh0N@H)|kkp^YewIW*bRduq=QXn#;aD;^C}_eOPj~V37$nkEKd|8X(`|AM^&u)BN+^ z_cG#2!}3tskf8HLxr5c%%P;`Dpsr1?vRHG~tFRq>d0R^U4CE1!Qy}GM4E7b2zsR@u zhsY8?-k&75`NjT)k=0}Zzfm?@!hVvY>}?<`M*R*lMDe_Zy-_|g5Iy)~w4VpYl7cC` zO4dm&2@|#ioTM^3%D#@+Z)_YnMn^~B0Z-Ha8FCKl)lOY^dVT)|fu3VD delta 4237 zcma)9Yit|G5xzYh$rE3aXo?gmks>MTK|LwS@*}q6mn_FG)rs9GrC+7ACzlpQ*?T9) zQIC)n*|A;JiQG-bV`aoNthZackvk$ar(ljX0qBDCk zrPu}<8=Re;{dQ(|W^QKnvzfn_{JZ>qj|BgI^3lzcn{N1{u0+O8OIx|3JDo;7+9y$sugKH#v=|dnH zy8S*0JBXYAOUdzW=Ub$i|H=6YY2zQb{*rD3*RVPyoj@$*%xtmDBEV)HtP#ag{x|mk z>E|i+STu=p*+x1_T6q=ooZ3f*_`B*`u`F)tLgK9wA96kX+cjEqbva9H{Q|WDhXG36dBTsoEycCV_L*D4Ns=<5C1JF(I(`6to zycb@ZZ2*#W-?{tuycyES-}9!)7T%YPa>ciYWcXro9Y5g0;*Zv*B3>xc0f*ycNjPgt%P4@A5`^4xmL_MlDYl7!8jLq!f?Ce0!la>FuCud`YfNW*c-OjP3lp$1Spx+B zq06uaIN+xrc1n^VogtMPN-7>ISGNlh8>p5F*C*^;a~>+dyd-M88tm%=oK_%dW2Wq6+b0>Je-Y87^)dq zA|ui=IdQZS1`j5d$%Rq=LAa5>7H;s@PAkg}rW}@*9p@DOt8lNs#cWx2=*O4kbAK>B zyeZPGU?};v$TsKGsk48Uzn}$_jN? z5~k;>WCV>mGqOaMh?%@fmK?Z>_;Crabz%m_xVJGqvgQuK7eiO1D+KEMI_kNk8g5fE z$&x$*`ScR0q|6j0;2?!9(@-T8eP2#mr$_ z7i`V4>8NT>n`xoh$?8CJ8a2?U(O{-9XtW*z*kGmwA6p4xiiW_NlO3#DYq}G}BT}|` z%q}zpzL0shZWN3;{egKonS6GO!BWb$4-fIhy}@V6ee^wjC-~q!OFv$k@OXvO~$B@q> zIgSK7hqyrAT{JW{Q@CJxOU3e8HhUW9te=0}+)m28DV~jLh@C=$KC{S~ymDTfoMapM zi8%No#-ENSQmY<8XIS1-c=AEeH#_wt2=ur4&*R0-F5)2y{P&O;3Bs6`!$ehjhzs~6 zQAvRGkS>97Nr+5iB3T}5NfJNb(sHW73lZ0`HcCVWpaMU3k-yfm zOT7p(Y^{7C*T4fw|GIjFssgHlC55m>Xo&|_fs4u3b>X!jAA+8|{o`aOaf$3X0NK+4 zUAewpG!D4CNDR>x?#?7I)W&zG-)zG;{Xb+UPq%(~!EzMKQ*h?bv!e?SYIlB?L<<4? z6|@Mv<#Wd}d{>040Y)Q9!oyf0o0I_)_*k>$HQ3s5+)nLU*D1acYCZI^6 zY>nN0w{sx7u?HcxHA5$yFqHefv8Q=RAnh`K$5;+nh#sD3CEk{*otqO64Uq3az%X;vKilE9fWi z%;BD$eQR{F8$z$8Xk|KZKV>HgPkO`rw><;B_ikg~Kz*LxpYxcA!jQSW=>nbjL->+Oui>cAF}+?4|2S%rtXJNo-khEFxip=(+D0cj@; zCc;X#=4;@wr!jcH>C8?7{z_k}-_BN4fT4gt0EA;W3WRrjz**`{VH#e&6Z&5Mai2zR z@_hfx!;c~6OGq9Ba_5yODypchqN0l0dICZCwqqxu`lN};kLFV3d44|kc=zh3_dEiI zP?gjEyzWj=4$t&P7gW&m+SGOQn+w2_QzdnTy})-5Tw6E*^HBy%c6U1p&vl<(oPpdKn^oP^jtU)`xZ>VS-Ab~0E=2Aj#UjcoERV9mNI)5nvke9 zN)d_;JBs@k&?PnQ$tNaD#d+-(e|0EJZt>p@EsTm2pk4UW=YFO{5fS!oA!xlnL#UqrV7>Ri>v-b;$Rq`OMV+jY5NRgtMUZ5bu`#v;47+si%rQ1L3LpRK@_Mce z@2@+Ia8XpxAomDAIXp-v`HkVeg%k=zw{AmDv{B3oyO)bUB{0>+Ur9`4{uoZjkzn<< zOWsA~7Lkb0={j=HAi0S|q}mI}VL0KvKq*5%z" - ] - }, - "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]